---

Step * of Lemma p-id-compose

∀[A,B:Type]. ∀[f:A ⟶ (B + Top)].  (p-id() o f = f ∈ (A ⟶ (B + Top)))
BY
{ (Auto
   THEN Unfold `p-compose` 0
   THEN Ext
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Try ((Fold `p-compose` 0 THEN Auto))
   THEN SplitOnConclITE
   THEN Auto) }

1
.....truecase..... 
1. A : Type
2. B : Type
3. f : A ⟶ (B + Top)
4. x : A
5. ↑can-apply(f;x)
⊢ (p-id() do-apply(f;x)) = (f x) ∈ (B + Top)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].    (p-id()  o  f  =  f)


By

---

Latex:
(Auto
  THEN  Unfold  `p-compose`  0
  THEN  Ext
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((Fold  `p-compose`  0  THEN  Auto))
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index