(* ok *)
alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
alias R             /Coq/Reals/Rdefinitions/R.con
alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
alias R1            /Coq/Reals/Rdefinitions/R1.con
alias R0            /Coq/Reals/Rdefinitions/R0.con
alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
(eqT R
  (Rplus R1 R1)
  (Rmult R1 R1))