proposition: Lemma ref_R2 C D a : D \in Req C -> gen (D,aR a) -> gen (C,a).
proof: Proof. case/fsetU1P => [->|]; first by constructor. case/fimsetP => u. rewrite inE andbC. case: (isDiaP _) => //= s -> inC -> H. rewrite (fset1U inC). by constructor. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def demo gen_def relaxed_pruning)