---

Step * 1 1 of Lemma not_bfalse_btrue_const_fn_equal_union

.....assertion..... 
1. (x.tt) = (x.ff)@i
 0 = 1
BY
{ (Unfold `b-union` (1) THEN (Assert (x.tt) = (x.ff) BY Auto)) }

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

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


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


By

(Unfold  `b-union`  (1)\mcdot{}  THEN  (Assert  (\mlambda{}x.tt)  =  (\mlambda{}x.ff)  BY  Auto))



Home Index