---

Step * of Lemma assert-eq-lnk

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

---

Latex:


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


By

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

---

Home Index