proposition: Lemma evalDist_seq_eq : forall (A1 A2 B : Set)(c1 c2 : Comp B)(f1 : B -> Comp A1)(f2 : B -> Comp A2) y z, (forall x : B, evalDist c1 x == evalDist c2 x) -> (forall x : B, In x (getSupport c1) -> evalDist (f1 x) y == evalDist (f2 x) z) -> evalDist (x <-$ c1; f1 x) y == evalDist (x <-$ c2; f2 x) z.
proof: Proof. intuition. eapply (distro_iso_eq (fun b => b)(fun b => b)); intuition. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eauto. rewrite H. trivial. eapply H0. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eauto. rewrite <- H. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia