---

Step * of Lemma assert_of_tt

↑tt
BY
{ (Rewrite assert_evalC 0 THEN Auto{1,4}-1) }

---

Latex:

---

Latex:
\muparrow{}tt


By

---

Latex:
(Rewrite  assert\_evalC  0  THEN  Auto\{1,4\}-1)

---

Home Index