---

Step * of Lemma seteqweaken_wf

∀s1,s2:coSet{i:l}.  (seteqweaken(s2) ∈ (s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
BY
{ (Auto THEN ((Subst' seteqweaken(s2) ~ TERMOF{seteqweaken1_ext:o, \\v:l, i:l} s1 s2 0 THENA Computation) THENM Auto)) }

---

Latex:

---

Latex:
\mforall{}s1,s2:coSet\{i:l\}.    (seteqweaken(s2)  \mmember{}  (s1  =  s2)  {}\mRightarrow{}  seteq(s1;s2))


By

---

Latex:
(Auto
  THEN  ((Subst'  seteqweaken(s2)  \msim{}  TERMOF\{seteqweaken1\_ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  s1  s2  0  THENA  Computation)
            THENM  Auto
            )
  )

---

Home Index