COND_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Simplifies conditional terms.
DESCRIPTION
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.
HOL  Kananaskis-13