---

Step * 1 of Lemma sublist_antisymmetry


1. T : Type
2. L1 : T List
3. L2 : T List
4. L1 ⊆ L2
5. L2 ⊆ L1
⊢ ||L1|| = ||L2|| ∈ ℤ
BY
{ (AllHyps (\i. (FwdThruLemma `length_sublist` [i] THENA Auto)) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  L1  \msubseteq{}  L2
5.  L2  \msubseteq{}  L1
\mvdash{}  ||L1||  =  ||L2||


By

---

Latex:
(AllHyps  (\mbackslash{}i.  (FwdThruLemma  `length\_sublist`  [i]  THENA  Auto))  THEN  Auto')

---

Home Index