---

Step * of Lemma list_ind-general-wf

∀[A:Type]. ∀[B:(A List) ⟶ ℙ]. ∀[x:B[[]]]. ∀[F:∀a:A. ∀L:A List.  (B[L] ⇒ B[[a / L]])]. ∀[L:A List].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B[L])
BY
{ (Auto THEN Unhide THEN MoveToConcl (-1)) }

1
1. A : Type
2. B : (A List) ⟶ ℙ
3. x : B[[]]
4. F : ∀a:A. ∀L:A List.  (B[L] ⇒ B[[a / L]])
⊢ ∀L:A List. (rec-case(L) of [] => x | h::t => r.F[h;t;r] ∈ B[L])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:(A  List)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x:B[[]]].  \mforall{}[F:\mforall{}a:A.  \mforall{}L:A  List.    (B[L]  {}\mRightarrow{}  B[[a  /  L]])].  \mforall{}[L:A  List].
    (rec-case(L)  of
      []  =>  x
      h::t  =>
        r.F[h;t;r]  \mmember{}  B[L])


By

---

Latex:
(Auto  THEN  Unhide  THEN  MoveToConcl  (-1))

---

Home Index