---

Step * of Lemma p-first-cons

∀[A,B:Type]. ∀[L:(A ⟶ (B + Top)) List]. ∀[f:A ⟶ (B + Top)].  (p-first([f / L]) = [f?p-first(L)] ∈ (A ⟶ (B + Top)))
BY
{ (Auto THEN Subst' [f / L] ~ [f] @ L 0 THEN Try (Complete ((Reduce 0 ⋅ THEN Auto)))) }

1
1. A : Type
2. B : Type
3. L : (A ⟶ (B + Top)) List
4. f : A ⟶ (B + Top)
⊢ p-first([f] @ L) = [f?p-first(L)] ∈ (A ⟶ (B + Top))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:(A  {}\mrightarrow{}  (B  +  Top))  List].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].    (p-first([f  /  L])  =  [f?p-first(L)])


By

---

Latex:
(Auto  THEN  Subst'  [f  /  L]  \msim{}  [f]  @  L  0  THEN  Try  (Complete  ((Reduce  0  \mcdot{}  THEN  Auto))))

---

Home Index