---

Step * of Lemma sv-list-equal

∀T:Type. ∀L1,L2:T List. ∀x:T.
  (single-valued-list(L1;T)
  ⇒ single-valued-list(L2;T)
  ⇒ (x ∈ L1)
  ⇒ (x ∈ L2)
  ⇒ (||L1|| = ||L2|| ∈ ℤ)
  ⇒ (L1 = L2 ∈ (T List)))
BY
{ ((Auto
    THEN BLemma `list_extensionality`
    THEN Auto
    THEN All (Unfold `single-valued-list`)
    THEN (InstHyp [⌜x⌝;⌜L1[i]⌝] (-7)⋅ THENA (Auto THEN GenListD 0))
    THEN (InstHyp [⌜x⌝;⌜L2[i]⌝] (-7)⋅ THENA (Auto THEN GenListD 0))
    THEN Auto)
   THEN ListInd (-1)
   ) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L1,L2:T  List.  \mforall{}x:T.
    (single-valued-list(L1;T)
    {}\mRightarrow{}  single-valued-list(L2;T)
    {}\mRightarrow{}  (x  \mmember{}  L1)
    {}\mRightarrow{}  (x  \mmember{}  L2)
    {}\mRightarrow{}  (||L1||  =  ||L2||)
    {}\mRightarrow{}  (L1  =  L2))


By

---

Latex:
((Auto
    THEN  BLemma  `list\_extensionality`
    THEN  Auto
    THEN  All  (Unfold  `single-valued-list`)
    THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L1[i]\mkleeneclose{}]  (-7)\mcdot{}  THENA  (Auto  THEN  GenListD  0))
    THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L2[i]\mkleeneclose{}]  (-7)\mcdot{}  THENA  (Auto  THEN  GenListD  0))
    THEN  Auto)
  THEN  ListInd  (-1)
  )

---

Home Index