proposition: Theorem DM_RC_G2_equiv : forall c x, evalDist (DM_RC_G1 c) x == evalDist (DM_RC_G2 c) (Some x).
proof: Proof. intuition. unfold DM_RC_G1, DM_RC_G2. comp_skip. comp_simp. comp_skip. dist_compute. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid