proposition: Lemma evalDist_ret_eq : forall (A : Set)(eqd1 eqd2 : eq_dec A) a1 a2 x, a1 = a2 -> evalDist (Ret eqd1 a1) x == evalDist (Ret eqd2 a2) x.
proof: Proof. intuition. simpl. subst. destruct (eqd1 a2 x); destruct (eqd2 a2 x); subst; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia