---

Step * of Lemma list_ind_reverse_wf_dependent

∀[A,B:Type].
  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀P:(A List) ⟶ B ⟶ ℙ.
    ((P [] nilcase)
    ⇒ (∀L:A List. ∀x:A. ∀b:B.  ((b = list_ind_reverse(L;nilcase;F) ∈ B) ⇒ (P L b) ⇒ (P (L @ [x]) (F b L x))))
    ⇒ (∀L:A List. (P L list_ind_reverse(L;nilcase;F))))
BY
{ (Auto
   THEN (Assert ∀n:ℕ. ∀LL:A List.  ((||LL|| = n ∈ ℕ) ⇒ (P LL list_ind_reverse(LL;nilcase;F))) BY
               (D 0 THENA Auto))⋅
   ) }

1
1. [A] : Type
2. [B] : Type
3. nilcase : B
4. F : B ⟶ (A List) ⟶ A ⟶ B
5. P : (A List) ⟶ B ⟶ ℙ
6. P [] nilcase
7. ∀L:A List. ∀x:A. ∀b:B.  ((b = list_ind_reverse(L;nilcase;F) ∈ B) ⇒ (P L b) ⇒ (P (L @ [x]) (F b L x)))
8. L : A List
9. n : ℕ
⊢ ∀LL:A List. ((||LL|| = n ∈ ℕ) ⇒ (P LL list_ind_reverse(LL;nilcase;F)))

2
1. [A] : Type
2. [B] : Type
3. nilcase : B
4. F : B ⟶ (A List) ⟶ A ⟶ B
5. P : (A List) ⟶ B ⟶ ℙ
6. P [] nilcase
7. ∀L:A List. ∀x:A. ∀b:B.  ((b = list_ind_reverse(L;nilcase;F) ∈ B) ⇒ (P L b) ⇒ (P (L @ [x]) (F b L x)))
8. L : A List
9. ∀n:ℕ. ∀LL:A List.  ((||LL|| = n ∈ ℕ) ⇒ (P LL list_ind_reverse(LL;nilcase;F)))
⊢ P L list_ind_reverse(L;nilcase;F)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}nilcase:B.  \mforall{}F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B.  \mforall{}P:(A  List)  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.
        ((P  []  nilcase)
        {}\mRightarrow{}  (\mforall{}L:A  List.  \mforall{}x:A.  \mforall{}b:B.
                    ((b  =  list\_ind\_reverse(L;nilcase;F))  {}\mRightarrow{}  (P  L  b)  {}\mRightarrow{}  (P  (L  @  [x])  (F  b  L  x))))
        {}\mRightarrow{}  (\mforall{}L:A  List.  (P  L  list\_ind\_reverse(L;nilcase;F))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  \mforall{}LL:A  List.    ((||LL||  =  n)  {}\mRightarrow{}  (P  LL  list\_ind\_reverse(LL;nilcase;F)))  BY
                          (D  0  THENA  Auto))\mcdot{}
  )

---

Home Index