---

Step * of Lemma decidable__equal_list

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀xs,ys:T List.  Dec(xs = ys ∈ (T List))))
BY
{ RepeatFor 2 (InductionOnList) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
⊢ Dec([] = [] ∈ (T List))

2
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. u : T@i
4. v : T List@i
5. Dec([] = v ∈ (T List))@i
⊢ Dec([] = [u / v] ∈ (T List))

3
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. u : T@i
4. v : T List@i
5. ∀ys:T List. Dec(v = ys ∈ (T List))@i
⊢ Dec([u / v] = [] ∈ (T List))

4
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. u : T@i
4. v : T List@i
5. ∀ys:T List. Dec(v = ys ∈ (T List))@i
6. u1 : T@i
7. v1 : T List@i
8. Dec([u / v] = v1 ∈ (T List))@i
⊢ Dec([u / v] = [u1 / v1] ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}xs,ys:T  List.    Dec(xs  =  ys)))


By

---

Latex:
RepeatFor  2  (InductionOnList)

---

Home Index