proposition: Lemma rel_sumList_compat : forall (A : Set)(f1 f2 : A -> Rat) ls rel, RatRel rel -> (forall a, In a ls -> rel (f1 a) (f2 a)) -> rel (sumList ls f1) (sumList ls f2).
proof: Proof. induction ls; intuition; simpl in *. unfold sumList; simpl. eapply refl. intuition. eapply trans. eapply refl. eapply sumList_cons. eapply trans. 2:{ eapply refl. symmetry. eapply sumList_cons. } eapply add_proper. intuition. eapply IHls; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms