proposition: Theorem G_hybrid_DistSingle_S_eq : forall i, Pr[G_hybrid (S i)] == Pr[DistSingle_G (B1 i) B2 c1].
proof: Proof. intuition. unfold G_hybrid, DistSingle_G, B1, B2. inline_first. comp_skip. comp_simp. eapply comp_spec_eq_impl_eq. destruct (lt_dec i (length l)). eapply comp_spec_eq_trans. eapply comp_spec_seq_eq; eauto with inhabited. eapply compMap_unroll_tl. rewrite firstn_length. eapply min_l. lia. intuition. eapply comp_spec_eq_refl. inline_first. rewrite firstn_firstn. comp_swap_r. comp_skip. inline_first. rewrite nth_firstn. comp_skip. comp_skip. rewrite <- app_assoc. rewrite <- app_comm_cons. simpl. eapply comp_spec_eq_refl. lia. lia. comp_irr_r. repeat rewrite firstn_ge_all. comp_skip. comp_skip. rewrite skipn_gt_nil in H3. simpl in *. intuition. subst. rewrite app_nil_r. eapply comp_spec_eq_refl. lia. lia. lia. Qed.
imports: FCF.FCF FCF.CompFold