---

Step * of Lemma injective-quotient_wf

∀[T,S:Type]. ∀[f:T ⟶ S].  (T//x.f[x] ∈ Type)
BY
{ ProveWfLemma }

1
1. T : Type
2. S : Type
3. f : T ⟶ S
⊢ EquivRel(T;x,y.f[x] = f[y] ∈ S)

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[f:T  {}\mrightarrow{}  S].    (T//x.f[x]  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index