### Nuprl Lemma : equal-by-name-cases

`∀a,x,y:Name.`
`  ∀T:Type. ∀z:T. ∀P,Q:ℙ. ∀t1:⋂p:P. T. ∀t2:⋂q:Q. T.`
`    (((a = x ∈ Name) ∧ P ∧ (z = t1 ∈ T)) ∨ ((a = y ∈ Name) ∧ Q ∧ (z = t2 ∈ T))`
`    `⇐⇒` (((a = x ∈ Name) ∧ P) ∨ ((a = y ∈ Name) ∧ Q)) ∧ (z = if name_eq(a;x) then t1 else t2 fi  ∈ T)) `
`  supposing ¬(x = y ∈ Name)`

Proof

Definitions occuring in Statement :  name_eq: `name_eq(x;y)` name: `Name` ifthenelse: `if b then t else f fi ` uimplies: `b supposing a` prop: `ℙ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` isect: `⋂x:A. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` prop: `ℙ` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` iff: `P `⇐⇒` Q` or: `P ∨ Q` cand: `A c∧ B` guard: `{T}` rev_implies: `P `` Q` bfalse: `ff` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  equal_wf name_wf name_eq_wf bool_wf eqtt_to_assert assert-name_eq eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination extract_by_obid isectElimination hypothesis rename unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination independent_pairFormation inlFormation productEquality independent_functionElimination inrFormation because_Cache dependent_pairFormation promote_hyp instantiate cumulativity isectEquality universeEquality

Latex:
\mforall{}a,x,y:Name.
\mforall{}T:Type.  \mforall{}z:T.  \mforall{}P,Q:\mBbbP{}.  \mforall{}t1:\mcap{}p:P.  T.  \mforall{}t2:\mcap{}q:Q.  T.
(((a  =  x)  \mwedge{}  P  \mwedge{}  (z  =  t1))  \mvee{}  ((a  =  y)  \mwedge{}  Q  \mwedge{}  (z  =  t2))
\mLeftarrow{}{}\mRightarrow{}  (((a  =  x)  \mwedge{}  P)  \mvee{}  ((a  =  y)  \mwedge{}  Q))  \mwedge{}  (z  =  if  name\_eq(a;x)  then  t1  else  t2  fi  ))
supposing  \mneg{}(x  =  y)

Date html generated: 2017_04_17-AM-09_17_37
Last ObjectModification: 2017_02_27-PM-05_21_54

Theory : decidable!equality

Home Index