proposition: Theorem GenSizedSuchThateq_proof A (n : A) `{Dec_Eq A} `{Gen A} `{Enum A}: GenSizedSuchThateq_manual n = @arbitrarySizeST _ (fun x => eq x n) _.
proof: Proof. reflexivity. Qed.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads