proposition: Lemma eq_annot_dec (E1 E2 : annot) : {E1 = E2} + {E1 <> E2}.
proof: Proof. decide equality; apply: eq_comparable. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CTL(CTL_def)