---

Step * of 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)
BY
{ ((UnivCD THENA Auto) THEN AutoSplit THEN Auto THEN SplitOrHyps THEN Auto) }

---

Latex:

---

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)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  AutoSplit  THEN  Auto  THEN  SplitOrHyps  THEN  Auto)

---

Home Index