---

Step * of Lemma stable__proj-eq

∀[n:ℕ]. ∀[a,b:ℙ^n].  Stable{a = b}
BY
{ (Auto THEN Unfold `proj-eq` 0 THEN Auto THEN RepeatFor 2 ((BLemma `stable__all` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbP{}\^{}n].    Stable\{a  =  b\}


By

---

Latex:
(Auto  THEN  Unfold  `proj-eq`  0  THEN  Auto  THEN  RepeatFor  2  ((BLemma  `stable\_\_all`  THEN  Auto)))

---

Home Index