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