proposition: Lemma semCheckableBoolSize (b : bool) size : semCheckableSize b size <-> b.
proof: Proof. rewrite /semCheckableSize /semCheckerSize /checker /testBool. split. - move => /(_ b) H. suff : [set true] b by move => <- //. eapply H. eexists (MkProp (MkRose (liftBool b) (lazy nil))). split. simpl. by rewrite -> (semReturnSize _ _ _). by eapply bool_successful. - move => Hb b' [qp [/semReturnSize <- <-]] /=. by rewrite bool_successful. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes