proposition: Lemma semChecker_def2 c : semChecker c <-> (forall qp, semProd c qp -> successful qp = true).
proof: Proof. rewrite /semChecker /semCheckerSize /semProd. split; intro H. - intros. destruct H0 as [s [H0 Ho']]. symmetry; eapply (H s). eexists. split; eauto. reflexivity. - intros n b [qp [H1 H2]]. symmetry in H2. rewrite H2. symmetry. apply H. eexists; eauto. split; eauto. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes