---

{ SQType(IdLnk) }

{ Proof }

---

Definitions occuring in Statement :  IdLnk: IdLnk,  sq_type: SQType(T)
Definitions :  sq_type: SQType(T),  IdLnk: IdLnk,  all: x:A. B[x],  implies: P  Q,  guard: {T},  member: t  T,  so_lambda: x.t[x],  prop: ,  pi1: fst(t),  so_apply: x[s],  pi2: snd(t)
Lemmas :  Id_sq,  pi1_wf,  Id_wf,  pi2_wf

---

SQType(IdLnk)


Date html generated: 2010_08_26-PM-11_32_05
Last ObjectModification: 2008_02_27-PM-09_22_04

Home Index