proposition: Lemma isBoxP s : isBox_spec s (isBox s).
proof: Proof. move: s => [ [|?|? ?|?] [|]] /=; try constructor. exact: isBox_true. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)