proposition: Lemma demoDD_S0 : demo DD S0.
proof: Proof. have lc C : C \in S0 -> lcons C by rewrite inE; bcase. have sub : {subset DD <= S0} by apply/subP; exact: prune_sub. by split; auto using fulfillsAR_DD, fulfillsAU_DD,AXn_complete_DD. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)