proposition: Lemma semImplicationSize {C} `{Checkable C} (c : C) (b : bool) s : semCheckerSize (implication b c) s <-> (b -> semCheckableSize c s).
proof: Proof. case: b; split=> //=; first by move/(_ refl_equal). by move => _ b [x [/semReturnSize <- <-]]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes