fact: Definition is_open : forall {gs}, goal gs -> M bool := mfix2 is_open (gs : _) (g : goal gs) : M _ := match g with | Metavar _ _ e | AnyMetavar _ _ e => M.is_evar e | @AHyp C f => M.nu Generate mNone (fun x : C => is_open _ (f x)) | HypLet A f => M.nu_let Generate f (fun _ : A =>is_open _) | HypRem _ g => is_open _ g | HypReplace _ _ g => is_open _ g end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef