proposition: Theorem count_occ_map x l: count_occ decA l x = count_occ decB (map l) (f x).
proof: Proof. revert x. induction l as [| a l' Hrec]; intro x; simpl. - reflexivity. - specialize (Hrec x). destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. + rewrite Hrec. reflexivity. + contradiction H2. rewrite H1. reflexivity. + specialize (Hfinjective H2). contradiction H1. + assumption. Qed.
imports: PeanoNat