---

Step * of Lemma inject-subtype

No Annotations
∀[C,A:Type].  ∀[B:Type]. ∀[f:A ⟶ B].  Inj(C;B;f) supposing Inj(A;B;f) supposing strong-subtype(C;A)
BY
{ (Auto THEN RepeatFor 4 (ParallelLast) THEN Auto THEN InstLemma `strong-subtype-eq1` [⌜C⌝;⌜A⌝;⌜a1⌝;⌜a2⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C,A:Type].    \mforall{}[B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].    Inj(C;B;f)  supposing  Inj(A;B;f)  supposing  strong-subtype(C;A)


By

---

Latex:
(Auto
  THEN  RepeatFor  4  (ParallelLast)
  THEN  Auto
  THEN  InstLemma  `strong-subtype-eq1`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index