proposition: Lemma semChecker_def3 c : semChecker c <-> (successful @: semProd c \subset [set true]).
proof: Proof. rewrite semChecker_def2. split; intro H. - intros b H'. unfold imset, bigcup in H'. destruct H' as [qp [H1 H2]]. apply H in H1. by rewrite H1 in H2. - intros. specialize (H (successful qp)). unfold set1 in H. symmetry. apply: H. by eapply imset_in. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes