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