proposition: Lemma eq_form_dec (s t : form) : { s = t} + { s <> t}.
proof: Proof. decide equality; apply eq_comparable. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)