---

Step * of Lemma pair-blex_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index