---

Step * 1 of Lemma injective-quotient-inject


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))
BY
{ (Guard (-1) THEN RepeatFor 2 ((D 0 THENA Auto)) THEN Reduce 0 THEN (D 0 THENA (Unfold `guard` -3 THEN Auto))) }

1
1. T : Type
2. S : Type
3. f : T ⟶ S
4. {f ∈ T//x.f[x] ⟶ S}
5. a1 : T//x.f x
6. a2 : T//x.f x
7. (f a1) = (f a2) ∈ S
⊢ a1 = a2 ∈ T//x.f x

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [S]  :  Type
3.  [f]  :  T  {}\mrightarrow{}  S
4.  f  \mmember{}  T//x.f[x]  {}\mrightarrow{}  S
\mvdash{}  Inj(T//x.f  x;S;\mlambda{}x.(f  x))


By

---

Latex:
(Guard  (-1)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (D  0  THENA  (Unfold  `guard`  -3  THEN  Auto)))

---

Home Index