---

Step * 1 of Lemma remove_leading_wf


1. T : Type
2. P : T ⟶ 𝔹
⊢ remove_leading(x.P[x];[]) ∈ {L:T List| (¬↑null(L)) ⇒ (¬↑P[hd(L)])} 
BY
{ (RepUR ``remove_leading`` 0 THEN Auto THEN D -2 THEN All Reduce THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``remove\_leading``  0  THEN  Auto  THEN  D  -2  THEN  All  Reduce  THEN  Auto')

---

Home Index