proposition: Lemma semPredQPropSize (c : Checker) (s : nat) : semCheckableSize c s <-> (semCheckerSize c s).
proof: Proof. rewrite /semCheckableSize /checker /testChecker /checker /testProp /semCheckerSize. split; move => Hqp qp Hsize; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes