proposition: Lemma rel_seq : forall (A B C : Set)(c : Comp A)(f1 : A -> Comp B)(f2 : A -> Comp C) rel x1 x2, RatRel rel -> (forall a, In a (getSupport c) -> rel (evalDist (f1 a) x1) (evalDist (f2 a) x2)) -> rel (evalDist (a <-$ c; f1 a) x1) (evalDist (a <-$ c; f2 a) x2).
proof: Proof. intuition. simpl. eapply rel_sumList_compat; intuition. eapply mult_proper. eapply refl. intuition. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms