helm/matita/tests/replace.ma

   1 set "baseuri" "cic:/test".
   2 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
   3 alias num (instance 0) = "natural number".
   4 alias symbol "eq" (instance 0) = "leibnitz's equality".
   5 alias symbol "plus" (instance 0) = "natural plus".
   6 alias symbol "times" (instance 0) = "natural times".
   7 alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con".
   8 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
   9
  10 theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0).
  11  intro.
  12  replace in \vdash (? ? (? ? %) (? % %)) with x.
  13  reflexivity.
  14  rewrite < mult_n_O x.
  15  rewrite < plus_n_O x.
  16  reflexivity.
  17  reflexivity.
  18  auto.
  19 qed.