---

Step * of Lemma list_ind_wf

∀[A,B:Type]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B]. ∀[L:A List].  (rec-case(L) of [] => x | h::t => r.F[h;t;r] ∈ B)
BY
{ (Auto THEN InstLemma `list_ind-general-wf` [⌜A⌝;⌜λ2L.B⌝;⌜x⌝;⌜F⌝;⌜L⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `list\_ind-general-wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.B\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index