---

Step * 1 of Lemma co-list-islist-induction1


1. [A] : Type
2. [P] : co-list-islist(A) ⟶ ℙ
3. P[conil()]@i
4. ∀L:co-list-islist(A). ∀a:A.  (P[L] ⇒ P[cocons(a;L)])@i
5. L : co-list-islist(A)@i
⊢ P[L]
BY
{ (RenameVar `nilcase' 3
   THEN RenameVar `reccase' 4
   THEN UseWitness ⌜rec-case(L) of
                    [] => nilcase
                    a::t =>
                     r.reccase t a r⌝⋅
   THEN All (Unfolds ``all implies``)
   THEN Using [`B',⌜P⌝] (BLemma `list_ind-wf-co-list-islist2`)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [P]  :  co-list-islist(A)  {}\mrightarrow{}  \mBbbP{}
3.  P[conil()]@i
4.  \mforall{}L:co-list-islist(A).  \mforall{}a:A.    (P[L]  {}\mRightarrow{}  P[cocons(a;L)])@i
5.  L  :  co-list-islist(A)@i
\mvdash{}  P[L]


By

---

Latex:
(RenameVar  `nilcase'  3
  THEN  RenameVar  `reccase'  4
  THEN  UseWitness  \mkleeneopen{}rec-case(L)  of
                                    []  =>  nilcase
                                    a::t  =>
                                      r.reccase  t  a  r\mkleeneclose{}\mcdot{}
  THEN  All  (Unfolds  ``all  implies``)
  THEN  Using  [`B',\mkleeneopen{}P\mkleeneclose{}]  (BLemma  `list\_ind-wf-co-list-islist2`)\mcdot{}
  THEN  Auto)

---

Home Index