---

Step * 2 of Lemma not_bfalse_btrue_const_fn_equal_union

.....subterm..... T:t
2:n
x.tt  Base  (  )
BY
{ (BUnionRight THEN Auto) }


.....subterm.....  T:t
2:n
\mlambda{}x.tt  \mmember{}  Base  \mcup{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})


By

(BUnionRight  THEN  Auto)



Home Index