proposition: Lemma semResizeSizeEnum A (s n : nat) (g : E A) : semEnumSize (resize n g) s <--> semEnumSize g n.
proof: Proof. by case: g => g; rewrite /semEnumSize. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)