---

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

∀[A,B:Type]. ∀[L:(A ⟶ (B + Top)) List]. ∀[x:A].
  ∀[f:A ⟶ (B + Top)]. (do-apply(p-first(L);x) = do-apply(f;x) ∈ B) supposing ((↑can-apply(f;x)) and (f ∈ L)) 
  supposing (∀f,g∈L.  p-disjoint(A;f;g))
BY
{ xxx(Auto THEN RWO "do-apply-p-first" 0 THEN Auto)xxx }

1
.....rewrite subgoal..... 
1. A : Type
2. B : Type
3. L : (A ⟶ (B + Top)) List
4. x : A
5. (∀f,g∈L.  p-disjoint(A;f;g))
6. f : A ⟶ (B + Top)
7. (f ∈ L)
8. ↑can-apply(f;x)
⊢ ↑can-apply(p-first(L);x)

2
1. A : Type
2. B : Type
3. L : (A ⟶ (B + Top)) List
4. x : A
5. (∀f,g∈L.  p-disjoint(A;f;g))
6. f : A ⟶ (B + Top)
7. (f ∈ L)
8. ↑can-apply(f;x)
⊢ do-apply(hd(filter(λf.can-apply(f;x);L));x) = do-apply(f;x) ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:(A  {}\mrightarrow{}  (B  +  Top))  List].  \mforall{}[x:A].
    \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)]
        (do-apply(p-first(L);x)  =  do-apply(f;x))  supposing  ((\muparrow{}can-apply(f;x))  and  (f  \mmember{}  L)) 
    supposing  (\mforall{}f,g\mmember{}L.    p-disjoint(A;f;g))


By

---

Latex:
xxx(Auto  THEN  RWO  "do-apply-p-first"  0  THEN  Auto)xxx

---

Home Index