fact: Definition implication {prop : Type} `{Checkable prop} (b : bool) (p : prop) : Checker := if b then checker p else (returnGen (MkProp (returnRose rejected))).
imports: String List RoseTrees Show State Producer Generators Classes DependentClasses