---

Step * of Lemma assert-eq-id

∀[a,b:Id].  uiff(↑a = b;a = b ∈ Id)
BY
{ ((UnivCD THENA Auto) THEN Unfold `eq_id` 0 THEN GenConclAtAddr [1;1;1;1] THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:Id].    uiff(\muparrow{}a  =  b;a  =  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `eq\_id`  0
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index