---

Step * of Lemma proj-eq_weakening

∀[n:ℕ]. ∀[a,b:ℙ^n].  a = b supposing a = b ∈ ℙ^n
BY
{ (Auto THEN (RWO "-1" 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. a = b ∈ ℙ^n
⊢ b = b

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index