---

Step * 1 of Lemma cons_filter2

.....truecase..... 
1. T : Type
2. x : T
3. L : T List
4. P : ℕ||L|| + 1 ⟶ 𝔹
5. ↑(P 0)
⊢ [x / reduce2(λx,i,l. if P i then [x / l] else l fi ;[];1;L)] = [x / filter2(λi.(P (i + 1));L)] ∈ (T List)
BY
{ (EqCD THEN Auto THEN Unfold `filter2` 0 THEN Symmetry) }

1
1. T : Type
2. x : T
3. L : T List
4. P : ℕ||L|| + 1 ⟶ 𝔹
5. ↑(P 0)
⊢ reduce2(λx,i,l. if (λi.(P (i + 1))) i then [x / l] else l fi ;[];0;L)
= reduce2(λx,i,l. if P i then [x / l] else l fi ;[];1;L)
∈ (T List)

---

Latex:

---

Latex:
.....truecase..... 
1.  T  :  Type
2.  x  :  T
3.  L  :  T  List
4.  P  :  \mBbbN{}||L||  +  1  {}\mrightarrow{}  \mBbbB{}
5.  \muparrow{}(P  0)
\mvdash{}  [x  /  reduce2(\mlambda{}x,i,l.  if  P  i  then  [x  /  l]  else  l  fi  ;[];1;L)]  =  [x  /  filter2(\mlambda{}i.(P  (i  +  1));L)]


By

---

Latex:
(EqCD  THEN  Auto  THEN  Unfold  `filter2`  0  THEN  Symmetry)

---

Home Index