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