---

Step * of Lemma archive-condition-nil

∀[V:Type]. ∀A:Id List. ∀t:ℕ. ∀f:(V List) ─→ V. ∀n:ℤ. ∀v:V.  (archive-condition(V;A;t;f;n;v;[]) ⇐⇒ False)
BY
{ Auto }

1
1. V : Type
2. A : Id List@i
3. t : ℕ@i
4. f : (V List) ─→ V@i
5. n : ℤ@i
6. v : V@i
7. archive-condition(V;A;t;f;n;v;[])@i
⊢ False

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}n:\mBbbZ{}.  \mforall{}v:V.    (archive-condition(V;A;t;f;n;v;[])  \mLeftarrow{}{}\mRightarrow{}  False)


By

Auto

---

Home Index