proposition: Theorem DM_RC_G6_equiv : forall (c : A -> Comp B), evalDist (DM_RC_G5 c) (Some true) == evalDist (DM_RC_G6 c) true.
proof: Proof. unfold DM_RC_G5, DM_RC_G6. intuition. comp_skip. comp_simp. inline_first. comp_skip. rewrite compMap_head. comp_simp. destruct (hd_error (filter P x)). symmetry. rewrite <- evalDist_right_ident. comp_skip. dist_compute. dist_compute. intuition. Unshelve. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid