{ SQType(Kind) }
{ Proof }
Definitions occuring in Statement :
Kind: Kind,
sq_type: SQType(T)
Definitions :
tactic: Error :tactic,
CollapseTHEN: Error :CollapseTHEN,
Kind: Kind,
true: True,
btrue: tt,
bfalse: ff,
bool: 
,
inl: inl x ,
assert: 
b,
false: False,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
union: left + right,
pi1: fst(t),
IdLnk: IdLnk,
prop: 
,
limited-type: LimitedType,
pi2: snd(t),
so_lambda: 
x.t[x],
lambda: x.A[x],
universe: Type,
pair: <a, b>,
product: x:A 
B[x],
sqequal: s ~ t,
implies: P 
Q,
guard: {T},
member: t 
T,
equal: s = t,
Id: Id,
sq_type: SQType(T),
all: 
x:A. B[x],
function: x:A 
B[x]
Lemmas :
Id_sq,
Id_wf,
pi2_wf,
guard_wf,
pi1_wf,
IdLnk_sq,
IdLnk_wf,
decide_wf,
assert_wf,
bool_wf,
bfalse_wf,
btrue_wf
SQType(Kind)
Date html generated:
2010_08_26-PM-11_32_40
Last ObjectModification:
2009_10_14-PM-01_23_18
Home
Index