proposition: Lemma semForAllShrinkUnsized2 : forall {A C} `{Checkable C} `{Show A} (gen : G A) (f : A -> C) shrinker `{forall a, UnsizedChecker (checker (f a))}, (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'; last by eauto. eapply unsizedChecker_alt_def; 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