proposition: Theorem DM_RC_G4_equiv : forall c x, evalDist (DM_RC_G3 c) x == evalDist (DM_RC_G4 c) x.
proof: Proof. intuition. unfold DM_RC_G3, DM_RC_G4. comp_skip. symmetry. comp_simp. rewrite <- evalDist_assoc; intuition. comp_skip. eapply comp_spec_eq_impl_eq. eapply (@compMap_fission_eq _ _ _ _ _ _ _ _ _ _ _ _ eq); intuition. simpl. eapply comp_spec_eq_refl. subst. simpl. eapply eq_impl_comp_spec_eq. intuition. comp_at comp_inline rightc 1%nat. comp_swap_r. inline_first. comp_skip. comp_skip. comp_simp. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid