---

Step * 1 1 2 of Lemma not_bfalse_btrue_const_fn_equal_union


1. (x.tt) = (x.ff)@i
2. (x.tt) = (x.ff)
 0 = 1
BY
{ (Reduce (-1) THEN Auto) }

1
1. (x.tt) = (x.ff)@i
2. (x.tt) = (x.ff)
 0 = 1



1.  (\mlambda{}x.tt)  =  (\mlambda{}x.ff)@i
2.  (\mlambda{}x.tt)  =  (\mlambda{}x.ff)
\mvdash{}  0  =  1


By

(Reduce  (-1)  THEN  Auto)



Home Index