proposition: Lemma lcons_gen C a : ~~ lcons C -> gen (C,a).
proof: Proof. rewrite /lcons negb_and negbK. case/orP => [H|/allPn[s]]. - rewrite (fset1U H). by constructor. - case: s => [[|n|s t|s|s t|s t]] [|] //. rewrite negbK => H1 H2. rewrite (fset1U H1) (fset1U H2). 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)