---

Step * of Lemma can-apply-p-co-restrict

∀[A,B:Type]. ∀[f:A ⟶ (B + Top)]. ∀[P:A ⟶ ℙ]. ∀[p:∀x:A. Dec(P[x])]. ∀[x:A].
  uiff(↑can-apply(p-co-restrict(f;p);x);(↑can-apply(f;x)) ∧ (¬P[x]))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `p-co-restrict` 0
   THEN RWO "can-apply-compose-iff" 0
   THEN Auto
   THEN (All (RWO "do-apply-p-co-filter"))
   THEN Auto
   THEN (All (RWO "can-apply-p-co-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].
    uiff(\muparrow{}can-apply(p-co-restrict(f;p);x);(\muparrow{}can-apply(f;x))  \mwedge{}  (\mneg{}P[x]))


By

---

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

---

Home Index