proposition: Lemma lelistA_map A (R : relation A) B (S : relation B) (f : A->B) (f_mon : Proper (R ==> S) f) a : forall l, lelistA R a l -> lelistA S (f a) (map f l).
proof: Proof. induction l; intro h; simpl. apply nil_leA. inversion h; subst. apply cons_leA. apply f_mon. hyp. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil)