proposition: Lemma semForAllShrinkUnsized1 : forall {A C} `{Checkable C} `{Show A} (gen : G A) (f : A -> C) shrinker `{@Unsized _ _ ProducerGen gen}, (semChecker (forAllShrink gen shrinker f) <-> forall a : A, semProd gen a -> semCheckable (f a)).
proof: Proof. split=> H'. - move => a [s' [_ Hgen]] s. specialize (H' s). eapply semForAllShrinkSize in H'; first by eauto. eapply H1; eauto. - move => s; eapply semForAllShrinkSize; move => a Hgen. apply H'; eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes