proposition: Lemma map_inj {A B}: forall (f: A -> B), (forall x y, f x = f y -> x = y) -> (forall x y, (map f) x = (map f) y -> x = y).
proof: Proof. induction x; destruct y; simpl; intros HH; try congruence. inversion' HH; f_equal; eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists