Nuprl Lemma : assert-eq_var
∀a,b:varname(). uiff(↑eq_var(a;b);a = b ∈ varname())
Proof
Definitions occuring in Statement :
eq_var: eq_var(a;b),
varname: varname(),
assert: ↑b,
uiff: uiff(P;Q),
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
varname: varname(),
b-union: A ⋃ B,
tunion: ⋃x:A.B[x],
bool: 𝔹,
unit: Unit,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
eq_var: eq_var(a;b),
assert: ↑b,
bfalse: ff,
false: False,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
nat: ℕ,
band: p ∧b q,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
squash: ↓T,
true: True,
rev_uimplies: rev_uimplies(P;Q),
btrue: tt
Lemmas referenced :
istype-assert,
eq_var_wf,
assert_witness,
varname_wf,
assert_of_eq_atom,
assert_wf,
eq_atom_wf,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
eqtt_to_assert,
band_wf,
btrue_wf,
eq_int_wf,
bfalse_wf,
equal-wf-base,
atom_subtype_base,
set_subtype_base,
le_wf,
istype-int,
int_subtype_base,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_eq_int,
subtype_rel_b-union-left,
nat_wf,
subtype_rel_b-union-right,
assert_functionality_wrt_uiff,
squash_wf,
true_wf,
eq_atom-reflexive,
iff_imp_equal_bool,
iff_functionality_wrt_iff,
iff_weakening_equal,
istype-true,
assert_of_tt
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
independent_pairFormation,
isect_memberFormation_alt,
cut,
hypothesis,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
because_Cache,
independent_functionElimination,
equalityIstype,
inhabitedIsType,
universeIsType,
imageElimination,
productElimination,
unionElimination,
equalityElimination,
sqequalRule,
isatomReduceTrue,
independent_isectElimination,
voidElimination,
dependent_functionElimination,
instantiate,
cumulativity,
equalityTransitivity,
equalitySymmetry,
setElimination,
rename,
productEquality,
atomEquality,
applyEquality,
intEquality,
lambdaEquality_alt,
natural_numberEquality,
isect_memberEquality_alt,
productIsType,
sqequalBase,
promote_hyp,
independent_pairEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}a,b:varname(). uiff(\muparrow{}eq\_var(a;b);a = b)
Date html generated:
2020_05_19-PM-09_53_00
Last ObjectModification:
2020_03_09-PM-04_07_57
Theory : terms
Home
Index