---

Step * 1 1 1 1 2 of Lemma length-remove-first


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. (∃x∈v. ↑(P x)) ⇒ (||rec-case(v) of [] => [] | a::as => r.if P a then as else [a / r] fi || = (||v|| - 1) ∈ ℤ)
6. (∃x∈[u / v]. ↑(P x))
⊢ ||if P u then v else [u / rec-case(v) of [] => [] | h::t => r.if P h then t else [h / r] fi ] fi ||
= ((||v|| + 1) - 1)
∈ ℤ
BY
{ TACTIC:((RWO "l_exists_cons" (-1) THENA Auto) THEN D -1 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  (\mexists{}x\mmember{}v.  \muparrow{}(P  x))
{}\mRightarrow{}  (||rec-case(v)  of  []  =>  []  |  a::as  =>  r.if  P  a  then  as  else  [a  /  r]  fi  ||  =  (||v||  -  1))
6.  (\mexists{}x\mmember{}[u  /  v].  \muparrow{}(P  x))
\mvdash{}  ||if  P  u
then  v
else  [u  /  rec-case(v)  of  []  =>  []  |  h::t  =>  r.if  P  h  then  t  else  [h  /  r]  fi  ]
fi  ||
=  ((||v||  +  1)  -  1)


By

---

Latex:
TACTIC:((RWO  "l\_exists\_cons"  (-1)  THENA  Auto)  THEN  D  -1  THEN  AutoSplit)

---

Home Index