FLATTEN_CONJ_CONV : conv
STRUCTURE
unwindLib
SYNOPSIS
Flattens a ‘tree’ of conjunctions.
LIBRARY
unwind
DESCRIPTION
FLATTEN_CONJ_CONV "t1 /\ ... /\ tn" returns a theorem of the form: 
   |- t1 /\ ... /\ tn = u1 /\ ... /\ un
where the right-hand side of the equation is a flattened version of the left-hand side.
FAILURE
Never fails.
EXAMPLE
#FLATTEN_CONJ_CONV "(a /\ (b /\ c)) /\ ((d /\ e) /\ f)";;
|- (a /\ b /\ c) /\ (d /\ e) /\ f = a /\ b /\ c /\ d /\ e /\ f
HOL  Kananaskis-13