Nuprl Lemma : name_eq-normalize
∀[F,G,a,b:Top]. (if name_eq(a;b) then F a else G fi ~ if name_eq(a;b) then F b else G fi )
Proof
Definitions occuring in Statement :
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
and: P ∧ Q,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
uimplies: b supposing a,
sq-decider: sq-decider(eq),
name-deq: NameDeq,
list-deq: list-deq(eq),
list_ind: list_ind,
name_eq: name_eq(x;y)
Lemmas referenced :
top_wf,
ifthenelse_sqequal,
sq-decider-name-deq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
thin,
sqequalHypSubstitution,
hypothesis,
axiomSqEquality,
Error :inhabitedIsType,
hypothesisEquality,
Error :isect_memberEquality_alt,
isectElimination,
Error :isectIsTypeImplies,
Error :universeIsType,
extract_by_obid,
baseApply,
closedConclusion,
baseClosed,
independent_pairFormation,
Error :lambdaFormation_alt,
Error :productIsType,
sqequalIntensionalEquality,
independent_isectElimination,
independent_functionElimination
Latex:
\mforall{}[F,G,a,b:Top]. (if name\_eq(a;b) then F a else G fi \msim{} if name\_eq(a;b) then F b else G fi )
Date html generated:
2019_06_20-PM-01_58_06
Last ObjectModification:
2018_10_15-PM-02_19_57
Theory : decidable!equality
Home
Index