proposition: Lemma map_In_spec {A B : Type} (f : A -> B) (l : list A) : map_In l (fun (x : A) (_ : In x l) => f x) = List.map f l.
proof: Proof. funelim (map_In l _); rewrite ?H; trivial. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List