still some glitches, but reaching a decent state

[helm.git] / helm / software / matita / contribs / didactic / induction.ma

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index e2da2243ac90ede12b9d3be50969659b8fd71481..c4335ca3e313a15b55615084f12daa3f54a6a20c 100644 (file)
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -440,7 +440,7 @@ case FAtom.
      if eqb n x then G2 else (FAtom n)).
   case true.
     the thesis becomes (G1 ≡ G2).
-    done.
+    by H done.
   case false.
     (*BEGIN*)
     the thesis becomes (FAtom n ≡ FAtom n).