1\DOC COND_CONV
2
3\TYPE {COND_CONV : conv}
4
5\SYNOPSIS
6Simplifies conditional terms.
7
8\KEYWORDS
9conversion, conditional.
10
11\DESCRIBE
12The conversion {COND_CONV} simplifies a conditional term {"c => u | v"} if
13the condition {c} is either the constant {T} or the constant {F} or
14if the two terms {u} and {v} are equivalent up to alpha-conversion.
15The theorems returned in these three cases have the forms:
16{
17   |- (T => u | v) = u
18
19   |- (F => u | v) = u
20
21   |- (c => u | u) = u
22}
23
24
25\FAILURE
26{COND_CONV tm} fails if {tm} is not a conditional {"c => u | v"}, where
27{c} is {T} or {F}, or {u} and {v} are alpha-equivalent.
28
29\ENDDOC
30