---

Step * of Lemma not_bfalse_btrue_const_fn_equal_union

((x.tt) = (x.ff))
BY
{ (D 0 THEN Auto) }

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

2
.....subterm..... T:t
2:n
x.tt  Base  (  )

3
.....subterm..... T:t
3:n
x.ff  Base  (  )


\mneg{}((\mlambda{}x.tt)  =  (\mlambda{}x.ff))


By

(D  0  THEN  Auto)



Home Index