---

Step * of Lemma l-ordered-eq-rels

∀T:Type. ∀R1,R2:T ⟶ T ⟶ ℙ. ∀L:T List.
  ((∀x∈L.(∀y∈L.R1[x;y] ⇐⇒ R2[x;y])) ⇒ l-ordered(T;x,y.R1[x;y];L) ⇒ l-ordered(T;x,y.R2[x;y];L))
BY
{ (Auto
   THEN All(RepUR ``l-ordered``)
   THEN RepeatFor 3 (ParallelLast)
   THEN Repeat ((All (RWO "l_all_iff") THENA Auto))
   THEN InstHyp [⌜x⌝;⌜y⌝] (-7)⋅
   THEN Auto
   THEN Try (Complete ((FLemma `l_before_member` [-2] THEN Auto)))
   THEN Try (Complete ((FLemma `l_before_member2` [-2] THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L:T  List.
    ((\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.R1[x;y]  \mLeftarrow{}{}\mRightarrow{}  R2[x;y]))  {}\mRightarrow{}  l-ordered(T;x,y.R1[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R2[x;y];L))


By

---

Latex:
(Auto
  THEN  All(RepUR  ``l-ordered``)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Repeat  ((All  (RWO  "l\_all\_iff")  THENA  Auto))
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-7)\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((FLemma  `l\_before\_member`  [-2]  THEN  Auto)))
  THEN  Try  (Complete  ((FLemma  `l\_before\_member2`  [-2]  THEN  Auto))))

---

Home Index