Step
*
of Lemma
tuple-type-ext
∀[L,L':Type List]. tuple-type(L) ≡ tuple-type(L') supposing (||L|| = ||L'|| ∈ ℤ) ∧ (∀i:ℕ||L||. L[i] ≡ L'[i])
BY
{ (Auto THEN D 0 THEN Auto) }
Latex:
Latex:
\mforall{}[L,L':Type List].
tuple-type(L) \mequiv{} tuple-type(L') supposing (||L|| = ||L'||) \mwedge{} (\mforall{}i:\mBbbN{}||L||. L[i] \mequiv{} L'[i])
By
Latex:
(Auto THEN D 0 THEN Auto)
Home
Index