---

Step * of Lemma insert_int_nil_lemma

∀a:Top. (insert-int(a;[]) ~ [a])
BY
{ (UnivCD THENA Auto) }

1
1. a : Top
⊢ insert-int(a;[]) ~ [a]

---

Latex:

---

Latex:
\mforall{}a:Top.  (insert-int(a;[])  \msim{}  [a])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index