helm/matita/tests/rewrite.ma

   1 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
   2 alias num (instance 0) = "natural number".
   3 alias symbol "eq" (instance 0) = "leibnitz's equality".
   4 alias symbol "plus" (instance 0) = "natural plus".
   5
   6
   7 theorem a:
   8   \forall a,b:nat.
   9   a = b \to b + a + b + a= (\lambda j.((\lambda w.((\lambda x.x + b + w + j) a)) b)) a.
  10 intros.
  11 rewrite right H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)).
  12
  13 rewrite right H in \vdash (? ? % ?).
  14
  15 simplify in \vdash (? ? ? ((\lambda x.((\lambda y.%) ?)) ?)).
  16
  17 rewrite right H in \vdash (? ? ? (% ?)).
  18 simplify.
  19 reflexivity.
  20 qed.