---

Step * of Lemma list_eq_wf

∀[A:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. ∀[as,bs:A List].  (list_eq(eq;as;bs) ∈ 𝔹)
BY
{ (RepeatFor 2 (InductionOnList) THEN Unfold `list_eq` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as,bs:A  List].    (list\_eq(eq;as;bs)  \mmember{}  \mBbbB{})


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Unfold  `list\_eq`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index