---

{ [l:IdLnk]. l = l = tt }

{ Proof }

---

Definitions occuring in Statement :  eq_lnk: a = b,  IdLnk: IdLnk,  btrue: tt,  bool: ,  uall: [x:A]. B[x],  equal: s = t
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  uiff: uiff(P;Q),  and: P  Q,  uimplies: b supposing a,  rev_implies: P  Q,  iff: P  Q,  implies: P  Q
Lemmas :  eqtt_to_assert,  eq_lnk_wf,  iff_weakening_uiff,  assert_wf,  IdLnk_wf,  assert-eq-lnk

---

\mforall{}[l:IdLnk].  l  =  l  =  tt


Date html generated: 2011_08_10-AM-07_48_07
Last ObjectModification: 2011_06_18-AM-08_13_01

Home Index