---

Step * of Lemma mono-list

∀A:Type. (mono(A) ⇒ mono(A List))
BY
{ (Auto THEN D 0 THEN Auto THEN RepeatFor 2 (MoveToConcl (-1)) THEN ListInd (-1) THEN Auto) }

1
1. A : Type
2. mono(A)
3. b : Base
4. is-above(A List;[];b)
⊢ [] = b ∈ (A List)

2
1. A : Type
2. mono(A)
3. u : A
4. v : A List
5. ∀b:Base. (is-above(A List;v;b) ⇒ (v = b ∈ (A List)))
6. b : Base
7. is-above(A List;[u / v];b)
⊢ [u / v] = b ∈ (A List)

---

Latex:

---

Latex:
\mforall{}A:Type.  (mono(A)  {}\mRightarrow{}  mono(A  List))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RepeatFor  2  (MoveToConcl  (-1))  THEN  ListInd  (-1)  THEN  Auto)

---

Home Index