proposition: Lemma map_id' : forall `{f: A -> A} lst, (forall x, List.In x lst -> f x = x) -> map f lst = lst.
proof: Proof. induction lst; simpl; intros. - eauto. - f_equal; eauto. Qed.
imports: Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.AllOfLength CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.Zip2 Coq.Lists.List Coq.Program.Program