---

Step * 1 of Lemma list_ind-general-wf


1. A : Type
2. B : (A List) ⟶ ℙ
3. x : B[[]]
4. F : ∀a:A. ∀L:A List.  (B[L] ⇒ B[[a / L]])
⊢ ∀L:A List. (rec-case(L) of [] => x | h::t => r.F[h;t;r] ∈ B[L])
BY
{ ((Assert ⌜∀n:ℕ. ∀L:A List.  ((colength(L) = n ∈ ℤ) ⇒ (rec-case(L) of [] => x | h::t => r.F[h;t;r] ∈ B[L]))⌝⋅
   THENM (Auto THEN InstHyp [⌜colength(L)⌝;⌜L⌝] (-2)⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto
   THEN (FLemma `colength-zero` [-1] THENA Auto⋅ ORELSE FLemma `colength-positive2` [-1] THEN Auto⋅)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  (A  List)  {}\mrightarrow{}  \mBbbP{}
3.  x  :  B[[]]
4.  F  :  \mforall{}a:A.  \mforall{}L:A  List.    (B[L]  {}\mRightarrow{}  B[[a  /  L]])
\mvdash{}  \mforall{}L:A  List.  (rec-case(L)  of  []  =>  x  |  h::t  =>  r.F[h;t;r]  \mmember{}  B[L])


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}L:A  List.
                        ((colength(L)  =  n)  {}\mRightarrow{}  (rec-case(L)  of  []  =>  x  |  h::t  =>  r.F[h;t;r]  \mmember{}  B[L]))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}colength(L)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto
  THEN  (FLemma  `colength-zero`  [-1]  THENA  Auto\mcdot{}  ORELSE  FLemma  `colength-positive2`  [-1]  THEN  Auto\mcdot{})
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index