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