---

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


1. A : Type
2. B : Type
⊢ ∀[x:A]. do-apply(p-first([]);x) = do-apply(hd(filter(λf.can-apply(f;x);[]));x) ∈ B supposing ↑can-apply(p-first([]);x)
BY
{ xxx(Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}[x:A]
        do-apply(p-first([]);x)  =  do-apply(hd(filter(\mlambda{}f.can-apply(f;x);[]));x) 
        supposing  \muparrow{}can-apply(p-first([]);x)


By

---

Latex:
xxx(Reduce  0  THEN  Auto)xxx

---

Home Index