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)).
+interpretation "megacoso" '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)).
render cic:/Coq/Arith/Plus/plus_comm.con.
# full samples