---

Step * of Lemma test-change-equality

∀[L1:ℕ List]. ∀[L2:ℤ List].  ((L1 = L2 ∈ (ℤ List)) ⇒ (L1 = L2 ∈ (ℕ List)))
BY
{ Intros }

1
1. L1 : ℕ List
2. L2 : ℤ List
3. L1 = L2 ∈ (ℤ List)
⊢ L1 = L2 ∈ (ℕ List)

---

Latex:

---

Latex:
\mforall{}[L1:\mBbbN{}  List].  \mforall{}[L2:\mBbbZ{}  List].    ((L1  =  L2)  {}\mRightarrow{}  (L1  =  L2))


By

---

Latex:
Intros

---

Home Index