---

Step * of Lemma pair-lex_wf

∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].  (pair-lex(A;Ra;Rb) ∈ (A × B) ⟶ (A × B) ⟶ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].    (pair-lex(A;Ra;Rb)  \mmember{}  (A  \mtimes{}  B)  {}\mrightarrow{}  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index