proposition: Theorem compMap_computeHybrid_n_equiv : forall s_A a, Pr [b <-$ compMap B_EqDec (fun _ : nat => (c1 a)) (forNats n); A2 s_A b ] == Pr [x <-$ computeHybrid n n a; A2 s_A x ].
proof: Proof. intuition. unfold computeHybrid. inline_first. comp_skip. inline_first. rewrite Nat.sub_diag. unfold forNats. unfold compMap. comp_simp. rewrite app_nil_r. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid