fact: Definition successful qp := match qp with | MkProp (MkRose res _) => resultSuccessful res end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes