proposition: Lemma evP C s : ev_case C s.
proof: Proof. Proof with try by apply: ev_x => G; rewrite /ev_cond. case: s => [[|x|s t|s|s t|s t]] [|]... - case: s => [|x|s t|s|s t|s t]... case: (boolP (C |> fAX (fAU s t)^+)) => /= E. case: (boolP (C |> s^+)) => E'. exact: ev_AU E' E. apply: ev_x => G; rewrite /ev_cond => ->. by rewrite E (negbTE E'). apply: ev_x => G; rewrite /ev_cond => ->. by rewrite (negbTE E). - case: s => [|x|s t|s|s t|s t]... case: (boolP (C |> fAX (fAR s t)^-)) => /= E. case: (boolP (C |> s^-)) => E'. exact: ev_AR E' E. apply: ev_x => G; rewrite /ev_cond => ->. by rewrite E (negbTE E'). apply: ev_x => G; rewrite /ev_cond => ->. by rewrite (negbTE E). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)