---

Step * of Lemma squash-assert

∀[b:𝔹]. uiff(↓↑b;↑b)
BY
{ (Unfold `assert` 0 THEN (D 0 THENA Auto) THEN AutoSplit THEN (RW (SubC SquashSimpC) 0 THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbB{}].  uiff(\mdownarrow{}\muparrow{}b;\muparrow{}b)


By

---

Latex:
(Unfold  `assert`  0  THEN  (D  0  THENA  Auto)  THEN  AutoSplit  THEN  (RW  (SubC  SquashSimpC)  0  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index