{L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    {ϕ : L →ᴸ L'} →
      {motive : ϕ.Injective → Sort u_1} →
        (t : ϕ.Injective) →
          ((onFunction : ∀ {n : ℕ}, Function.Injective fun f => ϕ.onFunction f) →
              (onRelation : ∀ {n : ℕ}, Function.Injective fun R => ϕ.onRelation R) → motive ⋯) →
            motive t