{ 
[M:Type 
Type]
S1,S2:System(P.M[P]). sub-system(P.M[P];S1;S2) supposing S1 = S2 }
{ Proof }
Definitions occuring in Statement :
sub-system: sub-system(P.M[P];S1;S2),
System: System(P.M[P]),
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
function: x:A B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
System: System(P.M[P]),
so_apply: x[s],
uimplies: b supposing a,
sub-system: sub-system(P.M[P];S1;S2),
and: P 
Q,
member: t 
T,
top: Top,
subtype: S 
T,
so_lambda: 
x.t[x],
cand: A c B,
prop: 
,
ldag: LabeledDAG(T),
pi1: fst(t),
pi2: snd(t)
Lemmas :
pi1_wf_top,
pi2_wf,
sublist_weakening,
component_wf,
lg-contains_weakening,
labeled-graph_wf,
ldag_wf,
pInTransit_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}S1,S2:System(P.M[P]). sub-system(P.M[P];S1;S2) supposing S1 = S2
Date html generated:
2011_08_17-PM-03_47_01
Last ObjectModification:
2011_06_18-AM-11_27_09
Home
Index