proposition: Lemma map_id `(f : A -> A) (Hf : forall x, f x = x) (l : list A) : map f l = l.
proof: Proof. induction l as [|x l IHl]. - reflexivity. - simpl. rewrite Hf,IHl. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra