helm/gTopLevel/esempi/ring/caso3.1bis.cic

   1 (* ok *)
   2 alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
   3 alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
   4 alias R             /Coq/Reals/Rdefinitions/R.con
   5 alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
   6 alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
   7 alias R1            /Coq/Reals/Rdefinitions/R1.con
   8 alias R0            /Coq/Reals/Rdefinitions/R0.con
   9 alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
  10 alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
  11 alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
  12 alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
  13 alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
  14 alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
  15 alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
  16 alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
  17 alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
  18 alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
  19 alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
  20 alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
  21 alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
  22 alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
  23 (eqT R
  24   (Rplus R1 R1)
  25   (Rmult R1 R1))