2 lines
174 B
Text
2 lines
174 B
Text
@eq.{1} nat (@add.{0} nat nat_has_add2 a b) (@add.{0} nat nat_has_add2 a b)
|
|
@eq.{1} (nat → nat) (λ (x : nat), @add.{0} nat nat_has_add2 a b) (@add.{0} nat nat_has_add2 a)
|