proposition: Theorem DM_RC_G5_equiv : forall (c : A -> Comp B) x, evalDist (DM_RC_G4 c) x == evalDist (DM_RC_G5 c) x.
proof: Proof. intuition. unfold DM_RC_G4, DM_RC_G5. comp_skip. comp_simp. comp_skip. symmetry. eapply eqRat_trans. comp_skip. eapply compMap_filter. intuition. eapply eqRat_refl. inline_first. comp_skip. dist_compute. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid