{A : Type} (f : A -> A) (l : list A) (Hf : forall x, InList x l -> f x = x) : list_map f l = l. Proof. induction l as [|x l IHl]. - reflexivity. - simpl. nrapply ap011. + exact (Hf _ (inl idpath)). + apply IHl. intros y Hy. apply Hf. by right. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum