proposition: Theorem G2_2_3_eq_until_bad : forall z, evalDist G2_2 (z, false) == evalDist G2_3 (z, false).
proof: Proof. pose proof RF_Encrypt_wf. intuition. unfold G2_2, G2_3. do 3 (comp_skip; comp_simp). unfold PRFE_RandomFunc, randomFunc. case_eq (arrayLookup (Bvector_EqDec eta) l x ); intuition. comp_simp. comp_irr_r; wftac. comp_irr_l; wftac. eapply oc_comp_wf; intuition. comp_irr_r; wftac. eapply oc_comp_wf; intuition. comp_simp. Local Transparent evalDist. Local Transparent getSupport. dist_compute. Local Opaque evalDist. Local Opaque getSupport. inline_first. comp_skip. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime