---

Step * of Lemma assert-eq-knd

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

---

Latex:


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


By

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

---

Home Index