proposition: Lemma semForAllSizeMonotonic {A C} `{Show A, Checkable C} (g : G A) (f : A -> C) `{@SizeMonotonic _ _ ProducerGen g} `{forall a, SizeMonotonicChecker (checker (f a))} : (semChecker (forAll g f) <-> forall (a:A), a \in semProd g -> semCheckable (f a)).
proof: Proof. split; move => Hcheck a. - move => [s [_ H']] s'. case_eq (s <= s') => [/leP Hleq | /leP/Compare_dec.not_le/ltP/ltnW Hleq]. + specialize (Hcheck s'). rewrite -> semForAllSize in Hcheck. apply Hcheck. eapply monotonic; eauto. + specialize (Hcheck s). eapply semForAllSize in Hcheck; eauto. by eapply monotonicChecker_alt_def; eauto. - by eapply semForAllSize; intros; apply Hcheck; eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes