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