---

Step * of Lemma order-preserving_wf

∀[A,B:Type]. ∀[R1:A ⟶ A ⟶ ℙ]. ∀[R2:B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B].
  (order-preserving(A;B;a1,a2.R1[a1;a2];b1,b2.R2[b1;b2];f) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R1:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R2:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:A  {}\mrightarrow{}  B].
    (order-preserving(A;B;a1,a2.R1[a1;a2];b1,b2.R2[b1;b2];f)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index