Nuprl Lemma : name_eq-normalize3
∀[F,G,X,a,b:Top].
(case name_eq(a;b) ∧b X of inl(x) => F[a] | inr(y) => G ~ case name_eq(a;b) ∧b X of inl(x) => F[b] | inr(y) => G)
Proof
Definitions occuring in Statement :
name_eq: name_eq(x;y),
band: p ∧b q,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
sqequal: s ~ t
Definitions unfolded in proof :
so_apply: x[s],
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas referenced :
name_eq-normalize2,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache,
isect_memberFormation,
introduction,
sqequalAxiom,
sqequalRule,
isect_memberEquality
Latex:
\mforall{}[F,G,X,a,b:Top].
(case name\_eq(a;b) \mwedge{}\msubb{} X of inl(x) => F[a] | inr(y) => G \msim{} case name\_eq(a;b) \mwedge{}\msubb{} X
of inl(x) =>
F[b]
| inr(y) =>
G)
Date html generated:
2016_05_14-PM-03_34_52
Last ObjectModification:
2015_12_26-PM-05_59_50
Theory : decidable!equality
Home
Index