---

Step * of Lemma linorder_functionality_wrt_ext-eq

∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ].  Linorder(A;x,y.R[x;y]) ⇐⇒ Linorder(B;x,y.R[x;y]) supposing A ≡ B
BY
{ (Auto THEN RepeatFor 11 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    Linorder(A;x,y.R[x;y])  \mLeftarrow{}{}\mRightarrow{}  Linorder(B;x,y.R[x;y])  supposing  A  \mequiv{}  B


By

---

Latex:
(Auto  THEN  RepeatFor  11  (ParallelLast))

---

Home Index