proposition: Lemma residualP (f : nat -> word char) (L : lang char) : (forall n1 n2, residual L (f n1) =p residual L (f n2) -> n1 = n2) -> ~ inhabited (regular L).
proof: Proof. move => f_spec [[A E]]. pose f' (n : 'I_#|A|.+1) := delta_s A (f n). suff: injective f' by move/leq_card; rewrite card_ord ltnn. move => [n1 H1] [n2 H2]. rewrite /f' /delta_s /= => H. apply/eqP; change (n1 == n2); apply/eqP. apply: f_spec => w. by rewrite /residual !E !inE /dfa_accept !delta_cat H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)