fact: Definition change_dep {X} (B : X -> Type) x {y} (f : ttac (B x)) : ttac (B y) := ( e <- M.unify x y UniCoq; match e with | mSome e => match e in Logic.meq _ z return ttac (B z) with | Logic.meq_refl => f end | mNone => M.raise TTchange_Exception end )%MC.
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String