---

Step * 1 of Lemma inject_functionality


1. A : Type
2. B : Type
3. C : Type
4. f : B ⟶ C
5. strong-subtype(A;B)
6. A ⊆r B
7. Inj(B;C;f)
⊢ Inj(A;C;f)
BY
{ (RepeatFor 4 (ParallelLast)⋅ THEN FLemma `strong-subtype-implies` [5] THEN Auto THEN BHyp (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  B  {}\mrightarrow{}  C
5.  strong-subtype(A;B)
6.  A  \msubseteq{}r  B
7.  Inj(B;C;f)
\mvdash{}  Inj(A;C;f)


By

---

Latex:
(RepeatFor  4  (ParallelLast)\mcdot{}
  THEN  FLemma  `strong-subtype-implies`  [5]
  THEN  Auto
  THEN  BHyp  (-1)
  THEN  Auto)

---

Home Index