---

Step * 2 1 1 of Lemma do-apply-p-first-disjoint


1. A : Type
2. B : Type
⊢ ∀x:A. ∀f:A ⟶ (B + Top).
    ((∀f,g∈[].  p-disjoint(A;f;g))
    ⇒ (f ∈ [])
    ⇒ (↑can-apply(f;x))
    ⇒ (hd(filter(λf.can-apply(f;x);[])) = f ∈ (A ⟶ (B + Top))))
BY
{ xxx(Unfold `pairwise` 0 THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}x:A.  \mforall{}f:A  {}\mrightarrow{}  (B  +  Top).
        ((\mforall{}f,g\mmember{}[].    p-disjoint(A;f;g))
        {}\mRightarrow{}  (f  \mmember{}  [])
        {}\mRightarrow{}  (\muparrow{}can-apply(f;x))
        {}\mRightarrow{}  (hd(filter(\mlambda{}f.can-apply(f;x);[]))  =  f))


By

---

Latex:
xxx(Unfold  `pairwise`  0  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index