-interpretation "Rtwo" 'two =
- (cic:/matita/demo/power_derivative/Rplus.con
- cic:/matita/demo/power_derivative/R1.con
- cic:/matita/demo/power_derivative/R1.con).
-interpretation "Ntwo" 'two =
- (cic:/matita/nat/nat/nat.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)))).