Nuprl Lemma : strong_subtype_decidable_eq
A,B:Type. (strong-subtype(A;B) 
dec_eq_type(B) dec_eq_type(A))
Proof
Definitions occuring in Statement :
dec_eq_type: dec_eq_type(T),
all: x:A. B[x],
implies: P Q,
universe: Type,
strong-subtype: strong-subtype(A;B)
Definitions :
all: x:A. B[x],
implies: P Q,
strong-subtype: strong-subtype(A;B),
dec_eq_type: dec_eq_type(T),
cand: A c
B,
exists: 
x:A. B[x],
decidable: Dec(P),
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
or: P 
Q,
squash: 
T,
true: True,
guard: {T},
not: 
A,
uall: [x:A]. B[x],
so_apply: x[s],
false: False
Lemmas :
all_wf,
or_wf,
equal_wf,
not_wf,
exists_wf,
member_wf,
squash_wf,
true_wf
\mforall{}A,B:Type. (strong-subtype(A;B) {}\mRightarrow{} dec\_eq\_type(B) {}\mRightarrow{} dec\_eq\_type(A))
Date html generated:
2013_03_20-AM-09_45_54
Last ObjectModification:
2012_12_07-AM-00_12_30
Home
Index