{T : Type u_1} →
  {N : Type u_2} →
    {r : ContextFreeRule T N} →
      {motive : (a a_1 : List (Symbol T N)) → r.Rewrites a a_1 → Prop} →
        {a a_1 : List (Symbol T N)} → r.Rewrites a a_1 → Prop