proposition: Lemma isBoxP a s : isBox_spec a s (isBox a s).
proof: Proof. move: s => [ [|?|? ?|[b|? ?|? ?|?|?|?] ?] [|]] /=; try constructor. case H: (a == b); try constructor. rewrite (eqP H). by exact: isBox_true. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)