---

Step * of Lemma can-apply-compose-iff

∀[A,B,C:Type]. ∀[g:A ⟶ (B + Top)]. ∀[f:B ⟶ (C + Top)]. ∀[x:A].
  uiff(↑can-apply(f o g;x);(↑can-apply(g;x)) ∧ (↑can-apply(f;do-apply(g;x))))
BY
{ (RepeatFor 2 (Auto) THEN ∀h:hyp. ((FLemma `can-apply-compose` [h]) THEN Auto) ) }

1
1. A : Type
2. B : Type
3. C : Type
4. g : A ⟶ (B + Top)
5. f : B ⟶ (C + Top)
6. x : A
7. ↑can-apply(g;x)
8. ↑can-apply(f;do-apply(g;x))
⊢ ↑can-apply(f o g;x)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[g:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[f:B  {}\mrightarrow{}  (C  +  Top)].  \mforall{}[x:A].
    uiff(\muparrow{}can-apply(f  o  g;x);(\muparrow{}can-apply(g;x))  \mwedge{}  (\muparrow{}can-apply(f;do-apply(g;x))))


By

---

Latex:
(RepeatFor  2  (Auto)  THEN  \mforall{}h:hyp.  ((FLemma  `can-apply-compose`  [h])  THEN  Auto)  )

---

Home Index