---

Step * of Lemma p-first-append

∀[A,B:Type]. ∀[L1,L2:(A ⟶ (B + Top)) List].
  (p-first(L1 @ L2) = p-first([p-first(L1); p-first(L2)]) ∈ (A ⟶ (B + Top)))
BY
{ (Auto THEN Ext THEN Auto) }

1
1. A : Type
2. B : Type
3. L1 : (A ⟶ (B + Top)) List
4. L2 : (A ⟶ (B + Top)) List
5. x : A
⊢ (p-first(L1 @ L2) x) = (p-first([p-first(L1); p-first(L2)]) x) ∈ (B + Top)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L1,L2:(A  {}\mrightarrow{}  (B  +  Top))  List].
    (p-first(L1  @  L2)  =  p-first([p-first(L1);  p-first(L2)]))


By

---

Latex:
(Auto  THEN  Ext  THEN  Auto)

---

Home Index