Nuprl Lemma : not_base_decidble_eq_diag2
(t1,t2:Base.  Dec(t1 = t2))
Proof
Definitions occuring in Statement : 
decidable: Dec(P), 
all: x:A. B[x], 
not: A, 
base: Base, 
equal: s = t
Definitions : 
so_lambda: x.t[x], 
member: t  T, 
implies: P  Q, 
not: A, 
ifthenelse: if b then t else f fi , 
rev_implies: P  Q, 
and: P  Q, 
or: P  Q, 
prop: , 
it: , 
bfalse: ff, 
btrue: tt, 
unit: Unit, 
isl: isl(x), 
assert: b, 
iff: P  Q, 
bool: , 
exists: x:A. B[x], 
decidable: Dec(P), 
all: x:A. B[x], 
false: False, 
true: True, 
so_apply: x[s], 
uall: [x:A]. B[x], 
uiff: uiff(P;Q), 
uimplies: b supposing a, 
guard: {T}, 
sq_type: SQType(T)
Lemmas : 
equal_wf, 
decidable_wf, 
base_wf, 
all_wf, 
assert_wf, 
iff_wf, 
false_wf, 
true_wf, 
bfalse_wf, 
bool_wf, 
btrue_wf, 
not_wf, 
or_wf, 
subtype_rel_self, 
isl_wf, 
assert_of_bnot, 
eqff_to_assert, 
bnot_wf, 
ext-eq_weakening, 
subtype_rel_weakening, 
uiff_transitivity, 
eqtt_to_assert, 
bool_subtype_base, 
subtype_base_sq, 
bool_cases, 
assert_elim, 
Error :not_id_sqeq_bottom, 
and_wf, 
not_assert_elim
\mneg{}(\mforall{}t1,t2:Base.    Dec(t1  =  t2))
Date html generated:
2013_03_20-AM-09_47_58
Last ObjectModification:
2012_11_27-AM-10_32_00
Home
Index