proposition: Theorem inSupportRandomPerm : forall a b r, In r (getSupport (getUnusedR a)) -> a # b = None -> In ((b, r) :: a, r) (getSupport (randomPerm (a, b))).
proof: Proof. intuition. unfold randomPerm. rewrite H0. eapply getSupport_In_Seq. eauto. simpl. intuition. Qed.
imports: Crypto Permutation CompFold Array FCF State