Step
*
1
of Lemma
remove_leading_property
1. [T] : Type
2. P : T ⟶ 𝔹
⊢ ∃xs:{x:T| ↑P[x]}  List. ([] = (xs @ remove_leading(x.P[x];[])) ∈ (T List))
BY
{ xxx(RepUR ``remove_leading`` 0 THEN With ⌜[]⌝ (D 0)⋅ THEN Auto)xxx }
Latex:
Latex:
1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mexists{}xs:\{x:T|  \muparrow{}P[x]\}    List.  ([]  =  (xs  @  remove\_leading(x.P[x];[])))
By
Latex:
xxx(RepUR  ``remove\_leading``  0  THEN  With  \mkleeneopen{}[]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx
Home
Index