{ 
[T:i:Id 
k:{k:Knd| 
hasloc(k;i)} Type]. [P:i:Id
k:{k:Knd| hasloc(k;i)}
T[i;k]]. [ik:LocKnd].
(let i,k:LocKnd = ik in P[i;k] 
T[fst(ik);snd(ik)]) }
{ Proof }
Definitions occuring in Statement :
locknd-spread: let i,k:LocKnd = ik in P[i; k],
LocKnd: LocKnd,
hasloc: hasloc(k;i),
Knd: Knd,
Id: Id,
assert: b,
uall: [x:A]. B[x],
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type
Definitions :
LocKnd: LocKnd,
locknd-spread: let i,k:LocKnd = ik in P[i; k],
uall: [x:A]. B[x],
so_apply: x[s1;s2],
member: t T,
pi1: fst(t),
pi2: snd(t),
prop: 
,
implies: P 
Q,
iff: P 
Q,
and: P 
Q,
rev_implies: P Q
Lemmas :
Id_wf,
Knd_wf,
assert_wf,
hasloc_wf
\mforall{}[T:i:Id {}\mrightarrow{} k:\{k:Knd| \muparrow{}hasloc(k;i)\} {}\mrightarrow{} Type]. \mforall{}[P:i:Id {}\mrightarrow{} k:\{k:Knd| \muparrow{}hasloc(k;i)\} {}\mrightarrow{} T[i;k]].
\mforall{}[ik:LocKnd].
(let i,k:LocKnd = ik in P[i;k] \mmember{} T[fst(ik);snd(ik)])
Date html generated:
2011_08_10-AM-07_51_52
Last ObjectModification:
2011_06_18-AM-08_14_15
Home
Index