---

Step * of Lemma taba_wf

∀[A,B:Type]. ∀[init:B]. ∀[F:A ⟶ A ⟶ B ⟶ B].  ∀xs:A List. (taba(init;x,x',a.F[x;x';a];xs) ∈ B)
BY
{ (Auto THEN Unfold `taba` 0) }

1
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
⊢ fst(rec-case(xs) of
      [] => <init, xs>
      x::xs' =>
       p.let a,ys = p 
         in let h,t = ys 
            in <F[x;h;a], t>) ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[init:B].  \mforall{}[F:A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].    \mforall{}xs:A  List.  (taba(init;x,x',a.F[x;x';a];xs)  \mmember{}  B)


By

---

Latex:
(Auto  THEN  Unfold  `taba`  0)

---

Home Index