Nuprl Lemma : alpha-eq-equiv-rel
∀[opr:Type]. EquivRel(term(opr);a,b.alpha-eq-terms(opr;a;b))
Proof
Definitions occuring in Statement :
alpha-eq-terms: alpha-eq-terms(opr;a;b),
term: term(opr),
equiv_rel: EquivRel(T;x,y.E[x; y]),
uall: ∀[x:A]. B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
equiv_rel: EquivRel(T;x,y.E[x; y]),
and: P ∧ Q,
refl: Refl(T;x,y.E[x; y]),
all: ∀x:A. B[x],
alpha-eq-terms: alpha-eq-terms(opr;a;b),
member: t ∈ T,
cand: A c∧ B,
sym: Sym(T;x,y.E[x; y]),
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
prop: ℙ,
trans: Trans(T;x,y.E[x; y])
Lemmas referenced :
alpha-aux-refl,
nil_wf,
varname_wf,
term_wf,
alpha-aux-symm,
alpha-eq-terms_wf,
istype-universe,
alpha-aux-trans
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
independent_pairFormation,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
hypothesis,
universeIsType,
because_Cache,
productElimination,
independent_functionElimination,
sqequalRule,
instantiate,
universeEquality
Latex:
\mforall{}[opr:Type]. EquivRel(term(opr);a,b.alpha-eq-terms(opr;a;b))
Date html generated:
2020_05_19-PM-09_55_39
Last ObjectModification:
2020_03_09-PM-04_09_00
Theory : terms
Home
Index