---

Step * of Lemma decidable__l_disjoint

∀[A:Type]. ((∀x,y:A.  Dec(x = y ∈ A)) ⇒ (∀L1,L2:A List.  Dec(l_disjoint(A;L1;L2))))
BY
{ InductionOnList }

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

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  ((\mforall{}x,y:A.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L1,L2:A  List.    Dec(l\_disjoint(A;L1;L2))))


By

---

Latex:
InductionOnList

---

Home Index