proposition: Theorem gen_complete C : gen (C,aVoid) + (exists (M:fmodel) (w:M), forall s, s \in C -> eval (interp' s) w).
proof: Proof. case: (fset0Vmem C) => [->|[s inC]]. - right. exists unit_model. exists tt => s. by rewrite inE. - pose sf := @closed_sfc C. have in_sfc : s \in sfc C by exact: (subP (@sub_sfc _)). have inU : C \in U (sfc C) by rewrite powersetE sub_sfc. case: (@ref_compl _ C _ sf in_sfc inU) => [ref_C|H];[left|right]. + exact: refpred_ref' ref_C. + move: H => [M] _ [w] ?. by exists M; exists w. 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)