fact: Definition is_prop_or_type (d : dyn) : t bool := mmatch d with | Dyn Prop => ret true | Dyn Type => ret true | _ => ret false end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)