---

Step * of Lemma dlattice-order_weakening

∀[X:Type]. ∀as,bs:X List List.  ((as = bs ∈ (X List List)) ⇒ as ⇒ bs)
BY
{ (Auto THEN (RWO "-1" 0 THENA Auto) THEN (D 0 THENA Auto) THEN D 0 With ⌜i⌝  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}as,bs:X  List  List.    ((as  =  bs)  {}\mRightarrow{}  as  {}\mRightarrow{}  bs)


By

---

Latex:
(Auto  THEN  (RWO  "-1"  0  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)

---

Home Index