proposition: Theorem G_hybrid_DistSingle_eq : forall i, Pr[G_hybrid i] == Pr[DistSingle_G (B1 i) B2 c2].
proof: Proof. intuition. unfold G_hybrid, DistSingle_G, B1, B2. inline_first. comp_skip. comp_simp. comp_swap_r. comp_skip. 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. intuition. eapply skipn_lt_nil_false; eauto. intuition. eapply comp_spec_eq_refl. inline_first. comp_skip. rewrite hd_skip_eq_nth. eapply comp_spec_eq_refl. subst. inline_first. rewrite tl_skipn_eq. comp_skip. rewrite skipn_gt_nil; intuition. simpl. comp_simp. rewrite app_nil_r. comp_irr_r. comp_irr_r. eapply compMap_wf. intuition. Qed.
imports: FCF.FCF FCF.CompFold