---

{ [T,S:Type].  T  S  Void supposing S  Void }

{ Proof }

---

Definitions occuring in Statement :  ext-eq: A  B,  uimplies: b supposing a,  uall: [x:A]. B[x],  product: x:A  B[x],  void: Void,  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  ext-eq: A  B,  and: P  Q,  member: t  T,  cand: A c B,  all: x:A. B[x],  implies: P  Q
Lemmas :  subtype_rel_wf,  uall_wf,  uiff_inversion,  member_wf,  ext-eq_inversion

---

\mforall{}[T,S:Type].    T  \mtimes{}  S  \mequiv{}  Void  supposing  S  \mequiv{}  Void


Date html generated: 2011_08_17-PM-06_58_21
Last ObjectModification: 2011_06_18-PM-12_37_12

Home Index