---

Step * of Lemma iseg_antisymmetry

∀[T:Type]. ∀[as,bs:T List].  (as = bs ∈ (T List)) supposing (bs ≤ as and as ≤ bs)
BY
{ xxx(((((InductionOnList THEN InductionOnList THEN Auto THEN (All (RWO "iseg_nil"))) THENM All Reduce)
        THEN Auto
        THEN (All (RWO "cons_iseg")))
      THENM All Reduce
      )
      THEN Auto
      THEN EqCD
      THEN Auto
      THEN BackThruSomeHyp
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (as  =  bs)  supposing  (bs  \mleq{}  as  and  as  \mleq{}  bs)


By

---

Latex:
xxx(((((InductionOnList  THEN  InductionOnList  THEN  Auto  THEN  (All  (RWO  "iseg\_nil")))
            THENM  All  Reduce
            )
            THEN  Auto
            THEN  (All  (RWO  "cons\_iseg")))
        THENM  All  Reduce
        )
        THEN  Auto
        THEN  EqCD
        THEN  Auto
        THEN  BackThruSomeHyp
        THEN  Auto)xxx

---

Home Index