proposition: Lemma semResizeSizeGen A (s n : nat) (g : G A) : semGenSize (resize n g) s <--> semGenSize g n.
proof: Proof. by case: g => g; rewrite /semGenSize. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)