---

Step * 3 of Lemma not_bfalse_btrue_const_fn_equal_union

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


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


By

(BUnionRight  THEN  Auto)\mcdot{}



Home Index