{T : Type u_1} →
  {N : Type u_2} →
    (motive : Symbol T N → Symbol T N → Sort u_3) →
      (x x_1 : Symbol T N) →
        ((a b : T) → motive (Symbol.terminal a) (Symbol.terminal b)) →
          ((t : T) → (n : N) → motive (Symbol.terminal t) (Symbol.nonterminal n)) →
            ((n : N) → (t : T) → motive (Symbol.nonterminal n) (Symbol.terminal t)) →
              ((a b : N) → motive (Symbol.nonterminal a) (Symbol.nonterminal b)) → motive x x_1