]> matita.cs.unibo.it Git - helm.git/commitdiff
completed test
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 8 Sep 2005 09:42:30 +0000 (09:42 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 8 Sep 2005 09:42:30 +0000 (09:42 +0000)
helm/matita/tests/unfold.ma

index 4af22f1b97c03796db9dc34dc34fd94099bc16b5..d63dd50d46d8a6a8027234ff691815f4a71c537b 100644 (file)
@@ -35,3 +35,5 @@ qed.
    not in the context of the goal. *)
 theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
  intros. unfold uno in H.
+ reflexivity.
+qed.