---

Step * of Lemma can-apply-p-restrict

∀[A,B:Type].
  ∀f:A ⟶ (B + Top)
    ∀[P:A ⟶ ℙ]. ∀p:∀x:A. Dec(P[x]). ∀x:A.  (↑can-apply(p-restrict(f;p);x) ⇐⇒ (↑can-apply(f;x)) ∧ P[x])
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `p-restrict` 0
   THEN RWO "can-apply-compose-iff" 0
   THEN Auto
   THEN (All (RWO "do-apply-p-filter"))
   THEN Auto
   THEN (All (RWO "can-apply-p-filter"))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}f:A  {}\mrightarrow{}  (B  +  Top)
        \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}]
            \mforall{}p:\mforall{}x:A.  Dec(P[x]).  \mforall{}x:A.    (\muparrow{}can-apply(p-restrict(f;p);x)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}can-apply(f;x))  \mwedge{}  P[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `p-restrict`  0
  THEN  RWO  "can-apply-compose-iff"  0
  THEN  Auto
  THEN  (All  (RWO  "do-apply-p-filter"))
  THEN  Auto
  THEN  (All  (RWO  "can-apply-p-filter"))
  THEN  Auto)

---

Home Index