COND_CONV
Conv.COND_CONV : conv
Simplifies conditional terms.
The conversion COND_CONV simplifies a conditional term "c => u | v"
if the condition c is either the constant T or the constant F or
if the two terms u and v are equivalent up to alpha-conversion. The
theorems returned in these three cases have the forms:
|- (T => u | v) = u
|- (F => u | v) = u
|- (c => u | u) = u
Failure
COND_CONV tm fails if tm is not a conditional "c => u | v", where
c is T or F, or u and v are alpha-equivalent.