proposition: Lemma map_congr : forall A B (f1 f2 : A->B) l, (forall x, Mem x l -> f1 x = f2 x) -> LibList.map f1 l = LibList.map f2 l.
proof: Proof. Proof using. #[global] Hint Constructors Exists. #[global] Hint Unfold Mem. introv H. induction l. auto. rew_listx. fequals~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat