{ 
[A:Type]. [B,eq,g:Top]. 
g }
{ Proof }
Definitions occuring in Statement :
fpf-sub: f g,
fpf-empty: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
universe: Type
Definitions :
isect: 
x:A. B[x],
void: Void,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
member: t 
T,
equal: s = t,
uall: [x:A]. B[x],
fpf-empty: ,
fpf-sub: f g,
lambda: 
x.A[x],
fpf_ap_pair: fpf_ap_pair{fpf_ap_pair_compseq_tag_def:o}(x; eq; f; d),
fpf-dom: x dom(f),
assert: 
b,
top: Top,
universe: Type,
all: x:A. B[x],
implies: P 
Q,
function: x:A 
B[x],
false: False,
prop: 
,
cand: A c
B,
product: x:A 
B[x],
Auto: Error :Auto,
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
top_wf,
assert_witness,
false_wf
\mforall{}[A:Type]. \mforall{}[B,eq,g:Top]. \motimes{} \msubseteq{} g
Date html generated:
2011_08_10-AM-07_57_04
Last ObjectModification:
2011_06_18-AM-08_17_27
Home
Index