proposition: Theorem comp_spec_irr_l : forall (A B C : Set){eqda : EqDec A}{eqdb : EqDec B}{eqdc : EqDec C}(c1 : Comp A)(c2 : Comp B)(f1 : A -> Comp C) P, well_formed_comp c1 -> (forall a, In a (getSupport c1) -> comp_spec P (f1 a) c2) -> comp_spec P (Bind c1 f1) c2.
proof: Proof. intuition. apply list_choice in H0. destruct H0. exists (y <-$ c1; x y). intuition. unfold marginal_l. dist_inline_first. dist_skip. specialize (H0 x0); intuition idtac. eapply H0. unfold marginal_r. dist_inline_first. dist_irr_r. specialize (H0 x0); intuition idtac. apply H2. repeat simp_in_support. specialize (H0 x0); intuition. intuition. eapply (EqDec_dec _). apply (x <-$ c1; y <-$ c2; z <-$ f1 x; ret (z, y)). Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1