---

Step * of Lemma l-ind_wf

∀[A,B:Type]. ∀[L:A List]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B].  (l-ind(L;x;h,t,r.F[h;t;r]) ∈ B)
BY
{ (Auto THEN Unhide THEN ListInd (-3) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[x:B].  \mforall{}[F:A  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  B  {}\mrightarrow{}  B].    (l-ind(L;x;h,t,r.F[h;t;r])  \mmember{}  B)


By

---

Latex:
(Auto  THEN  Unhide  THEN  ListInd  (-3)  THEN  Reduce  0  THEN  Auto)

---

Home Index