dest_disj : term -> term * term

SYNOPSIS

Breaks apart a disjunction into the two disjuncts.

DESCRIPTION

dest_disj is a term destructor for disjunctions:

   dest_disj `t1 \/ t2`

returns (`t1`,`t2`).

FAILURE CONDITIONS

Fails with dest_disj if term is not a disjunction.

SEE ALSO

is_disj, mk_disj.