proposition: Lemma bool_successful : forall b, resultSuccessful (liftBool b) = b.
proof: Proof. intros. destruct b; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes