helm/matita/tests/rewrite.ma

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