---

Step * of Lemma longest-prefix_wf

∀[T:Type]. ∀[L:T List]. ∀[P:T List+ ⟶ 𝔹].  (longest-prefix(P;L) ∈ T List)
BY
{ (InductionOnList
   THEN RecUnfold `longest-prefix` 0
   THEN RepUR ``let`` 0
   THEN Auto
   THEN Try (OnMaybeHyp 4 (\h. (InstHyp [⌜λL'.(P [u / L'])⌝] h⋅ THEN Complete (Auto))))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  List\msupplus{}  {}\mrightarrow{}  \mBbbB{}].    (longest-prefix(P;L)  \mmember{}  T  List)


By

---

Latex:
(InductionOnList
  THEN  RecUnfold  `longest-prefix`  0
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  Try  (OnMaybeHyp  4  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}\mlambda{}L'.(P  [u  /  L'])\mkleeneclose{}]  h\mcdot{}  THEN  Complete  (Auto)))))

---

Home Index