---

Step * of Lemma p-compose-associative

∀[A,B,C,D:Type]. ∀[h:A ⟶ (B + Top)]. ∀[g:B ⟶ (C + Top)]. ∀[f:C ⟶ (D + Top)].
  (f o g o h = f o g o h ∈ (A ⟶ (D + Top)))
BY
{ (Auto
   THEN Ext
   THEN Auto
   THEN RepUR ``p-compose can-apply do-apply`` 0
   THEN RepeatFor 2 ((((GenConclAtAddr [3; 1; 1]) THENA Auto) THEN D -2 THEN Reduce 0 THEN Try (Complete (Auto))))) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:Type].  \mforall{}[h:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[g:B  {}\mrightarrow{}  (C  +  Top)].  \mforall{}[f:C  {}\mrightarrow{}  (D  +  Top)].
    (f  o  g  o  h  =  f  o  g  o  h)


By

---

Latex:
(Auto
  THEN  Ext
  THEN  Auto
  THEN  RepUR  ``p-compose  can-apply  do-apply``  0
  THEN  RepeatFor  2  ((((GenConclAtAddr  [3;  1;  1])  THENA  Auto)
                                        THEN  D  -2
                                        THEN  Reduce  0
                                        THEN  Try  (Complete  (Auto)))))

---

Home Index