---

Step * of Lemma injective-quotient-inject

∀[T,S:Type]. ∀[f:T ⟶ S].  Inj(T//x.f[x];S;λx.f[x])
BY
{ (Unfold `so_apply` 0 THEN InstLemma `injective-quotient-typing` [] THEN RepeatFor 3 (ParallelLast')) }

1
1. [T] : Type
2. [S] : Type
3. [f] : T ⟶ S
4. f ∈ T//x.f[x] ⟶ S
⊢ Inj(T//x.f x;S;λx.(f x))

---

Latex:

---

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


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  InstLemma  `injective-quotient-typing`  []  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index