---

Step * of Lemma cons-sub-co-list-cons

∀[T:Type]
  ∀x1,x2:T. ∀L1,L2:colist(T).
    (sub-co-list(T;[x1 / L1];[x2 / L2]) ⇐⇒ ((x1 = x2 ∈ T) ∧ sub-co-list(T;L1;L2)) ∨ sub-co-list(T;[x1 / L1];L2))
BY
{ ((Unfold `cons` 0 THEN Fold `co-cons` 0) THEN Auto) }

1
1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : colist(T)
5. L2 : colist(T)
6. sub-co-list(T;[x1 / L1];[x2 / L2])
⊢ ((x1 = x2 ∈ T) ∧ sub-co-list(T;L1;L2)) ∨ sub-co-list(T;[x1 / L1];L2)

2
1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : colist(T)
5. L2 : colist(T)
6. ((x1 = x2 ∈ T) ∧ sub-co-list(T;L1;L2)) ∨ sub-co-list(T;[x1 / L1];L2)
⊢ sub-co-list(T;[x1 / L1];[x2 / L2])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}x1,x2:T.  \mforall{}L1,L2:colist(T).
        (sub-co-list(T;[x1  /  L1];[x2  /  L2])
        \mLeftarrow{}{}\mRightarrow{}  ((x1  =  x2)  \mwedge{}  sub-co-list(T;L1;L2))  \mvee{}  sub-co-list(T;[x1  /  L1];L2))


By

---

Latex:
((Unfold  `cons`  0  THEN  Fold  `co-cons`  0)  THEN  Auto)

---

Home Index