---

Step * of Lemma list-functionality-induction

∀T,A:Type. ∀F:Base.
  ((F[[]] ∈ A)
  ⇒ (∀a1,a2,L1,L2:Base.  ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A)))
  ⇒ (∀L:T List. (F[L] ∈ A)))
BY
{ (Auto THEN (PointwiseFunctionalityForEquality (-1) THENA Auto)) }

1
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. L : Base
7. L1 : Base
8. L = L1 ∈ (T List)
⊢ F[L] = F[L1] ∈ A

---

Latex:

---

Latex:
\mforall{}T,A:Type.  \mforall{}F:Base.
    ((F[[]]  \mmember{}  A)
    {}\mRightarrow{}  (\mforall{}a1,a2,L1,L2:Base.    ((a1  =  a2)  {}\mRightarrow{}  (F[L1]  =  F[L2])  {}\mRightarrow{}  (F[[a1  /  L1]]  =  F[[a2  /  L2]])))
    {}\mRightarrow{}  (\mforall{}L:T  List.  (F[L]  \mmember{}  A)))


By

---

Latex:
(Auto  THEN  (PointwiseFunctionalityForEquality  (-1)  THENA  Auto))

---

Home Index