---

Step * 1 of Lemma not_bfalse_btrue_const_fn_equal_union


1. (x.tt) = (x.ff)@i
 False
BY
{ (Assert 0 = 1 THEN Auto) }

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



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


By

(Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}  THEN  Auto)



Home Index