Nuprl Lemma : assert-C_TYPE_eq
∀[a,b:C_TYPE()]. uiff(↑C_TYPE_eq(a;b);a = b ∈ C_TYPE())
Proof
Definitions occuring in Statement :
C_TYPE_eq: C_TYPE_eq(a;b),
C_TYPE: C_TYPE(),
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
C_TYPE-induction,
uiff_wf,
assert_wf,
C_Struct?_wf,
bool_wf,
eqtt_to_assert,
eq_int_wf,
length_wf,
C_Struct-fields_wf,
assert_of_eq_int,
bl-all_wf,
int_seg_wf,
upto_wf,
l_member_wf,
eq_atom_wf,
select_wf,
sq_stable__le,
less_than_transitivity1,
le_weakening,
assert_of_eq_atom,
C_TYPE_eq_fun_wf,
equal_wf,
C_Struct_wf,
false_wf,
btrue_wf,
and_wf,
C_TYPE_wf,
bfalse_wf,
btrue_neq_bfalse,
equal-wf-T-base,
assert_witness,
l_all_wf2,
list_wf,
C_Array?_wf,
C_Array_wf,
nat_wf,
C_Pointer?_wf,
C_Pointer_wf,
all_wf,
squash_wf,
true_wf,
list_extensionality,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
less_than_wf,
assert-bl-all,
length_upto,
length_wf_nat,
lelt_wf,
select-upto,
equal-wf-base,
atom_subtype_base,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
list_subtype_base,
product_subtype_base,
C_TYPE_subtype_base,
pi1_wf_top,
subtype_rel_product,
top_wf,
subtype_top,
equal-wf-base-T,
pi2_wf,
C_Array-length_wf,
C_Array-elems_wf,
le_wf,
C_Pointer-to_wf
\mforall{}[a,b:C\_TYPE()]. uiff(\muparrow{}C\_TYPE\_eq(a;b);a = b)
Date html generated:
2015_07_17-AM-07_42_51
Last ObjectModification:
2015_01_27-AM-09_47_56
Home
Index