proposition: Lemma computes_under_bind X Y (f g : X -> Comp Y) x : (forall x, f x ~ g x) -> Bind x f ~ Bind x g.
proof: Proof. t; unfold equiv in *; split_iff; eauto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core