---

Step * of Lemma remove_leading_wf

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  (remove_leading(x.P[x];L) ∈ {L:T List| (¬↑null(L)) ⇒ (¬↑P[hd(L)])} )
BY
{ xxx(InductionOnList THEN Reduce 0 THEN (D 0 THENA Auto))xxx }

1
1. T : Type
2. P : T ⟶ 𝔹
⊢ remove_leading(x.P[x];[]) ∈ {L:T List| (¬↑null(L)) ⇒ (¬↑P[hd(L)])} 

2
1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. (remove_leading(x.P[x];v) ∈ {L:T List| (¬↑null(L)) ⇒ (¬↑P[hd(L)])} )
5. P : T ⟶ 𝔹
⊢ remove_leading(x.P[x];[u / v]) ∈ {L:T List| (¬↑null(L)) ⇒ (¬↑P[hd(L)])} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    (remove\_leading(x.P[x];L)  \mmember{}  \{L:T  List|  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (\mneg{}\muparrow{}P[hd(L)])\}  )


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0  THEN  (D  0  THENA  Auto))xxx

---

Home Index