@@ -114,7+114,11 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
-interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).