proposition: Lemma map_foldr {T1 T2} (f : T1 -> T2) xs : map f xs = foldr (fun x ys => f x :: ys) [::] xs.
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)