---

Step * of Lemma fun-equiv_wf

∀[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ]. ∀[f,g:X ⟶ A].  (fun-equiv(X;a,b.E[a;b];f;g) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[X,A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f,g:X  {}\mrightarrow{}  A].    (fun-equiv(X;a,b.E[a;b];f;g)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index