proposition: Lemma semCallback_id {C} `{Checkable C} (cb : Callback) (c : C) : semChecker (callback cb c) <-> semCheckable c.
proof: Proof. split => H' s; eapply semCallback_idSize; eauto. by apply H'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes