---

Step * of Lemma sublist-rec_wf

∀[T:Type]. ∀[l1,l2:T List].  (sublist-rec(T;l1;l2) ∈ ℙ)
BY
{ (Auto
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN RecUnfold `sublist-rec` 0
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].    (sublist-rec(T;l1;l2)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  RecUnfold  `sublist-rec`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index