- destruct tactic: automatic simplification in case of failure removed

[helm.git] / matita / library / demo / propositional_sequent_calculus.ma

diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index 32e11054c5d19bdb699f77578b4fa60fd1c83154..f68cfd22cbba1a47ac928e4b417073bbc00d4924 100644 (file)
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -433,7 +433,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
      |4,5:
        simplify in H2;
        destruct H2
-     | simplify in H2;
+     | simplify in H1;
        destruct H1
      ]
   |4,5: