---

Step * of Lemma l-ordered-no_repeats

∀[T:Type]. ∀[as:T List]. ∀[R:T ⟶ T ⟶ ℙ].
  (no_repeats(T;as)) supposing (l-ordered(T;x,y.R[x;y];as) and (∀x:T. (¬R[x;x])))
BY
{ xxx(Auto
      THEN BLemma `no_repeats_iff`
      THEN Auto
      THEN (InstHyp [⌜y⌝] 4)⋅
      THEN Auto
      THEN ParallelLast
      THEN Unfold `l-ordered` 5
      THEN (InstHyp [⌜x⌝; ⌜y⌝] 5)⋅
      THEN Auto
      THEN (HypSubst (-2) (-1))
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (no\_repeats(T;as))  supposing  (l-ordered(T;x,y.R[x;y];as)  and  (\mforall{}x:T.  (\mneg{}R[x;x])))


By

---

Latex:
xxx(Auto
        THEN  BLemma  `no\_repeats\_iff`
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  4)\mcdot{}
        THEN  Auto
        THEN  ParallelLast
        THEN  Unfold  `l-ordered`  5
        THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}]  5)\mcdot{}
        THEN  Auto
        THEN  (HypSubst  (-2)  (-1))
        THEN  Auto)xxx

---

Home Index