proposition: Lemma monotonicChecker_alt_def (c : Checker) `{SizeMonotonicChecker c} : forall s1 s2, s1 <= s2 -> semCheckerSize c s2 -> semCheckerSize c s1.
proof: Proof. rewrite /semCheckerSize => s1 s2 Hle. move : H => [/(_ s1 s2 Hle) H]. rewrite /genChecker in H; setoid_rewrite semFmapSize in H; eauto with typeclass_instances. move => H1 b H2. apply H1. eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes