proposition: Lemma regular_xm (char : finType) : (forall P, inhabited (regular (fun _ : word char => P))) <-> (forall P, P \/ ~ P).
proof: Proof. split => [H|H] P ; first exact: regular_det [::] (H P). case: (H P) => HP; constructor. + exists (dfa_compl (dfa_void char)) => x. by rewrite dfa_compl_correct dfa_void_correct. + exists (dfa_void char) => w. by rewrite /dfa_lang inE (negbTE (dfa_void_correct _ _)). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)