---

Step * of Lemma p-compose-inject

∀[A,B,C:Type]. ∀[g:A ⟶ (B + Top)]. ∀[f:B ⟶ (C + Top)].
  (p-inject(A;C;f o g)) supposing (p-inject(B;C;f) and p-inject(A;B;g))
BY
{ xxx(Auto
      THEN (All (Unfold `p-inject`))
      THEN Auto
      THEN (RWO "do-apply-compose" (-1))
      THEN Auto
      THEN RepeatFor 2 (((FLemma `can-apply-compose` [-3]) THENA Auto))
      THEN ((FHyp 7 [-3]) THENA Auto)
      THEN (FHyp 6 [-1])
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[g:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[f:B  {}\mrightarrow{}  (C  +  Top)].
    (p-inject(A;C;f  o  g))  supposing  (p-inject(B;C;f)  and  p-inject(A;B;g))


By

---

Latex:
xxx(Auto
        THEN  (All  (Unfold  `p-inject`))
        THEN  Auto
        THEN  (RWO  "do-apply-compose"  (-1))
        THEN  Auto
        THEN  RepeatFor  2  (((FLemma  `can-apply-compose`  [-3])  THENA  Auto))
        THEN  ((FHyp  7  [-3])  THENA  Auto)
        THEN  (FHyp  6  [-1])
        THEN  Auto)xxx

---

Home Index