proposition: Theorem G_2_hybrid_eq : Pr[ListHybrid_G c2] == Pr[G_hybrid 0].
proof: Proof. unfold ListHybrid_G, G_hybrid. comp_skip. comp_simp. eapply comp_spec_eq_impl_eq. simpl. comp_simp. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.CompFold