proposition: Lemma semForAllSize {A C} `{Show A, Checkable C} (g : G A) (f : A -> C) (s:nat) : semCheckerSize (forAll g f) s <-> forall (a : A), a \in semProdSize g s -> semCheckableSize (f a) s.
proof: Proof. split=> H'. - rewrite /forAll in H'. move/semBindGenSize : H' => H' a /H' Hgen. by apply semPrintTestCase_idSize in Hgen. - rewrite /forAll in H' *. apply semBindGenSize => g' Hgen. rewrite semPrintTestCase_idSize. by apply H'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes