Step
*
of Lemma
test-sq-stuff
∀L,L2:ℤ List. ((L = L2 ∈ (ℤ List))
⇒ (||L|| = ||L2|| ∈ ℤ))
BY
{ TACTIC:(UnivCD THENA Auto) }
1
1. L : ℤ List
2. L2 : ℤ List
3. L = L2 ∈ (ℤ List)
⊢ ||L|| = ||L2|| ∈ ℤ
Latex:
Latex:
\mforall{}L,L2:\mBbbZ{} List. ((L = L2) {}\mRightarrow{} (||L|| = ||L2||))
By
Latex:
TACTIC:(UnivCD THENA Auto)
Home
Index