(motive : Mathlib.Meta.FunProp.Origin → Sort u_1) →
  (origin : Mathlib.Meta.FunProp.Origin) →
    ((name : Lean.Name) → motive (Mathlib.Meta.FunProp.Origin.decl name)) →
      ((id : Lean.FVarId) → motive (Mathlib.Meta.FunProp.Origin.fvar id)) → motive origin