---

Step * of Lemma p-fun-exp-add1-sq

∀[A:Type]. ∀[f:A ⟶ (A + Top)]. ∀[x:A]. ∀[n:ℕ].  f^n + 1 x ~ f^n do-apply(f;x) supposing ↑can-apply(f;x)
BY
{ (Unfolds ``can-apply do-apply`` 0 THEN (UnivCD THENA Auto)) }

1
1. A : Type
2. f : A ⟶ (A + Top)
3. x : A
4. n : ℕ
5. ↑isl(f x)
⊢ f^n + 1 x ~ f^n outl(f x)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].  \mforall{}[x:A].  \mforall{}[n:\mBbbN{}].
    f\^{}n  +  1  x  \msim{}  f\^{}n  do-apply(f;x)  supposing  \muparrow{}can-apply(f;x)


By

---

Latex:
(Unfolds  ``can-apply  do-apply``  0  THEN  (UnivCD  THENA  Auto))

---

Home Index