proposition: Lemma semImplication {C} `{Checkable C} (c : C) (b : bool) : semChecker (implication b c) <-> (b -> semCheckable c).
proof: Proof. split; [move => H1 b' s' | move => H1 s b']; eapply semImplicationSize; try by eauto. move => b''. by apply H1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes