@eq.{1} nat (@has_add.add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b) (nat.add a b)
@eq.{1} (nat → nat)
  (λ (x : nat), @has_add.add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b)
  (nat.add a)
