---

Step * 1 of Lemma count-append


1. A : Type
2. P : A ⟶ 𝔹
3. L2 : A List
⊢ reduce(λa,n. (if P a then 1 else 0 fi  + n);0;L2) ~ 0 + reduce(λa,n. (if P a then 1 else 0 fi  + n);0;L2)
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
3.  L2  :  A  List
\mvdash{}  reduce(\mlambda{}a,n.  (if  P  a  then  1  else  0  fi    +  n);0;L2)  \msim{}  0  +  reduce(\mlambda{}a,n.  (if  P  a  then  1  else  0  fi    +  n\000C);0;L2)


By

---

Latex:
Auto

---

Home Index