---

Step * of Lemma ffor_wf

∀T:Type. ∀Q:(T List) ⟶ Type. ∀b0:Q[[]]. ∀b1:∀x:T. Q[[x]]. ∀up:∀ys,ys':T List.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys']).
∀zs:T List.
  (ffor(b0;b1;up;zs) ∈ Q[zs])
BY
{ (InductionOnList THEN RecUnfold `ffor` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}Q:(T  List)  {}\mrightarrow{}  Type.  \mforall{}b0:Q[[]].  \mforall{}b1:\mforall{}x:T.  Q[[x]].  \mforall{}up:\mforall{}ys,ys':T  List.
                                                                                                                                  (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  @  ys']).
\mforall{}zs:T  List.
    (ffor(b0;b1;up;zs)  \mmember{}  Q[zs])


By

---

Latex:
(InductionOnList  THEN  RecUnfold  `ffor`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index