-notation "14" non associative with precedence 80 for @{ 'x14 }.
-interpretation "natural number" 'x14 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
-
-notation "22" non associative with precedence 80 for @{ 'x22 }.
-interpretation "natural number" 'x22 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
-
-notation "30" non associative with precedence 80 for @{ 'x30 }.
-interpretation "natural number" 'x30 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))))))))))).
-
-notation "31" non associative with precedence 80 for @{ 'x31 }.
-interpretation "natural number" 'x31 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1))))))))))))))))))))))))))))))))).
-
-notation "32" non associative with precedence 80 for @{ 'x32 }.
-interpretation "natural number" 'x32 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))))))))))))).
-
-notation "255" non associative with precedence 80 for @{ 'x255 }.
-interpretation "natural number" 'x255 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
-
-notation "256" non associative with precedence 80 for @{ 'x256 }.
-interpretation "natural number" 'x256 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
-