proposition: Theorem G_1_hybrid_eq : Pr[ListHybrid_G c1] == Pr[G_hybrid maxA].
proof: Proof. unfold ListHybrid_G, G_hybrid. comp_skip. comp_simp. rewrite firstn_ge_all. comp_skip. rewrite skipn_ge_nil. eapply comp_spec_eq_impl_eq. simpl. comp_simp. rewrite app_nil_r. eapply comp_spec_eq_refl. eauto. eauto. Qed.
imports: FCF.FCF FCF.CompFold