---

Step * 1 1 1 of Lemma list-functionality-induction


1. T : Type
2. A : Type
3. F : Base
4. F[[]] ∈ A
5. ∀a1,a2,L1,L2:Base.  ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A))
6. n : ℤ
7. L : Base
8. L2 : Base
9. L = L2 ∈ (T List)
10. colength(L) = 0 ∈ ℤ
11. colength(L) = colength(L2) ∈ ℕ
⊢ F[L] = F[L2] ∈ A
BY
{ (((InstLemma `colength-zero` [⌜L⌝]⋅ THENM HypSubst' (-1) 0) THENA Auto)
   THEN (InstLemma `colength-zero` [⌜L2⌝]⋅ THENM HypSubst' (-1) 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  F  :  Base
4.  F[[]]  \mmember{}  A
5.  \mforall{}a1,a2,L1,L2:Base.    ((a1  =  a2)  {}\mRightarrow{}  (F[L1]  =  F[L2])  {}\mRightarrow{}  (F[[a1  /  L1]]  =  F[[a2  /  L2]]))
6.  n  :  \mBbbZ{}
7.  L  :  Base
8.  L2  :  Base
9.  L  =  L2
10.  colength(L)  =  0
11.  colength(L)  =  colength(L2)
\mvdash{}  F[L]  =  F[L2]


By

---

Latex:
(((InstLemma  `colength-zero`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENM  HypSubst'  (-1)  0)  THENA  Auto)
  THEN  (InstLemma  `colength-zero`  [\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENM  HypSubst'  (-1)  0)
  THEN  Auto)

---

Home Index