---

Step * of Lemma reject_wf

∀[A:Type]. ∀[l:A List]. ∀[n:ℤ].  (l\[n] ∈ A List)
BY
{ (Auto THEN (Decide ⌜n < 1⌝⋅ THENA Auto)) }

1
1. A : Type
2. l : A List
3. n : ℤ
4. n < 1
⊢ l\[n] ∈ A List

2
1. A : Type
2. l : A List
3. n : ℤ
4. ¬n < 1
⊢ l\[n] ∈ A List

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].  \mforall{}[n:\mBbbZ{}].    (l\mbackslash{}[n]  \mmember{}  A  List)


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}n  <  1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index