proposition: Lemma AXn_complete_DD : AXn_complete DD.
proof: Proof. move => L C /pruneE. rewrite !negb_or. case/and3P => [/hasPn H _ _] /H {H L}. rewrite negbK. case/hasP => L ? ?. by exists L; bcase. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)