---

{ b:. ((b = tt)  (b = ff)) }

{ Proof }

---

Definitions occuring in Statement :  bfalse: ff,  btrue: tt,  bool: ,  all: x:A. B[x],  or: P  Q,  equal: s = t
Definitions :  all: x:A. B[x],  member: t  T,  or: P  Q,  implies: P  Q,  prop: ,  guard: {T},  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  btrue: tt,  bfalse: ff,  it:
Lemmas :  bool_wf,  eqtt_to_assert,  btrue_wf,  bfalse_wf,  iff_transitivity,  assert_wf,  bnot_wf,  not_wf,  eqff_to_assert,  assert_of_bnot

---

\mforall{}b:\mBbbB{}.  ((b  =  tt)  \mvee{}  (b  =  ff))


Date html generated: 2010_08_27-AM-09_54_05
Last ObjectModification: 2009_12_17-PM-11_10_16

Home Index