---

Step * of Lemma eq_int_cases_test

∀[A:Type]. ∀x,y:A.  ∀[P:A ⟶ ℙ]. ∀i,j:ℤ.  ((P if (i =z j) then x else y fi ) ⇒ (P if (i =z j) then x else y fi ))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}x,y:A.
        \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}i,j:\mBbbZ{}.    ((P  if  (i  =\msubz{}  j)  then  x  else  y  fi  )  {}\mRightarrow{}  (P  if  (i  =\msubz{}  j)  then  x  else  y  fi  ))


By

---

Latex:
Auto

---

Home Index