dest_conj : term -> term * term
SYNOPSIS
Term destructor for conjunctions.
DESCRIPTION
dest_conj(`t1 /\ t2`)
returns
(`t1`,`t2`)
.
FAILURE CONDITIONS
Fails with
dest_conj
if term is not a conjunction.
SEE ALSO
is_conj
,
mk_conj
.