proposition: Lemma mono_step : monotone step.
proof: Proof. move => D D' /subP subD_D'. apply: sep_sub (subxx _) _ => A inU. case/or3P => H; apply/or3P; [apply: Or31|apply: Or32|apply: Or33]. - apply: in_sub_has H => s inF. do 2 apply: in_sub_has => ? ?. case (A == _) => //=. destruct s as [[|p|s t|s|s t|s t][|]] => //=; by [apply: subD_D'|case/andP => ? ?; apply/andP; split; exact: subD_D']. - case: A inU H => C [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] //= _. * case e: (C \in H); rewrite ?orbF // ?orbT. case/andP => ? ?; apply/andP; split; exact: subD_D'. * case e: (C \in H); rewrite ?orbF // ?orbT. case/andP => ? ?; apply/andP; split; exact: subD_D'. * exact: subD_D'. * case/orP => H; [leftb|rightb]; move: H. do 3 apply: in_sub_has => ? ?. case (C == _) => //=. exact: subD_D'. do 3 apply: in_sub_has => ? ?. case (C == _) => //=. exact: subD_D'. - case: A inU H => C E inU H. exact: subD_D'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)