X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=f68cfd22cbba1a47ac928e4b417073bbc00d4924;hb=5aa4da5846c72942f3d204f71ecfba8d6cc7911b;hp=32e11054c5d19bdb699f77578b4fa60fd1c83154;hpb=f1efdff5ded26d264f2848ff53c19fe2099682a3;p=helm.git

diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index 32e11054c..f68cfd22c 100644
--- 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: