{ 
[A:Type]. [B1,B2:A 
Type].
a:A fp-> B1[a] 
r a:A fp-> B2[a] supposing a:A. (B1[a] r B2[a]) }
{ Proof }
Definitions occuring in Statement :
fpf: a:A fp-> B[a],
subtype_rel: A r B,
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
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
all: x:A. B[x],
so_apply: x[s],
fpf: a:A fp-> B[a],
member: t 
T,
subtype: S T,
suptype: suptype(S; T),
so_lambda: 
x.t[x],
prop: 
Lemmas :
l_member_wf,
fpf_wf
\mforall{}[A:Type]. \mforall{}[B1,B2:A {}\mrightarrow{} Type]. a:A fp-> B1[a] \msubseteq{}r a:A fp-> B2[a] supposing \mforall{}a:A. (B1[a] \msubseteq{}r B2[a])
Date html generated:
2011_08_10-AM-07_54_33
Last ObjectModification:
2011_06_18-AM-08_15_04
Home
Index