proposition: Theorem G2_3_4_eq_until_bad : forall x, evalDist G2_3 (x, false) == evalDist G2_4 (x, false).
proof: Proof. intuition. unfold G2_3, G2_4. inline_first. comp_skip. inline_first. eapply comp_spec_impl_eq. comp_skip. eapply A_randomFunc_F_spec. simpl in *. comp_simp. eapply comp_spec_ret; intuition. pairInv. intuition. pairInv. trivial. pairInv. simpl in *. rewrite H3 in H4. intuition. pairInv. trivial. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv