!n:nat.(eq nat n n)

!n:nat.!m:nat.(eq nat n m)->(eq nat m n)

!n:nat.!m:nat.!p:nat.(eq nat n p)->(eq nat p m)->(eq nat n m)