---

Step * 1 of Lemma test-sq-stuff


1. L : ℤ List
2. L2 : ℤ List
3. L = L2 ∈ (ℤ List)
⊢ ||L|| = ||L2|| ∈ ℤ
BY
{ TACTIC:(RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  L2  :  \mBbbZ{}  List
3.  L  =  L2
\mvdash{}  ||L||  =  ||L2||


By

---

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

---

Home Index