---

Step * 2 of Lemma remove_leading_wf


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)])} 
BY
{ (Unfold `remove_leading` 0 THEN Reduce 0 THEN Fold `remove_leading` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  (remove\_leading(x.P[x];v)  \mmember{}  \{L:T  List|  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (\mneg{}\muparrow{}P[hd(L)])\}  )
5.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  remove\_leading(x.P[x];[u  /  v])  \mmember{}  \{L:T  List|  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (\mneg{}\muparrow{}P[hd(L)])\} 


By

---

Latex:
(Unfold  `remove\_leading`  0  THEN  Reduce  0  THEN  Fold  `remove\_leading`  0  THEN  AutoSplit)

---

Home Index