proposition: Lemma isCBoxP a s : isCBox_spec a s (isCBox a s).
proof: Proof. move: s => [ [|?|? ?|[b|? ?|? ?|?|?|p] ?] [|]] /=; try constructor. + case: p; try (move => *; constructor). move => b. case H: (a == b); try constructor. rewrite (eqP H). by apply: isCBox_true. + by case: p; constructor. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)