- 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 d79cd2e6ddded90916b5a01f48d00d305dafd225..f68cfd22cbba1a47ac928e4b417073bbc00d4924 100644 (file)
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -163,11 +163,10 @@ let rec and_of_list l ≝
   | cons F l' ⇒ FAnd F (and_of_list l')
   ].
 
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
 let rec or_of_list l ≝
  match l with
-  [ Nil ⇒ FFalse
-  | Cons F l' ⇒ FOr F (or_of_list l')
+  [ nil ⇒ FFalse
+  | cons F l' ⇒ FOr F (or_of_list l')
   ].
 
 definition formula_of_sequent ≝
@@ -434,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: