X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=f68cfd22cbba1a47ac928e4b417073bbc00d4924;hb=4c5f91917b06e323411981a22142bfedba996518;hp=4498676a3ef10f8a793464138f94e2638e130730;hpb=af130d273b6be7fbcc2fb2504f3b28ef8fa2344f;p=helm.git

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index 4498676a3..f68cfd22c 100644
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/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:
@@ -752,18 +751,18 @@ lemma completeness_base:
   [ decompose;
     rewrite > H2; clear H2;
     rewrite > H4; clear H4;
-    apply (exchangeL ? a1 a2 (FAtom a));
-    apply (exchangeR ? a3 a4 (FAtom a));
-    apply axiom 
+    apply (ExchangeL ? a1 a2 (FAtom a));
+    apply (ExchangeR ? a3 a4 (FAtom a));
+    apply Axiom 
   | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
      [ decompose;
        rewrite > H3;
-       apply (exchangeL ? a a1 FFalse);
-       apply falseL
+       apply (ExchangeL ? a a1 FFalse);
+       apply FalseL
      | decompose;
        rewrite > H3;
-       apply (exchangeR ? a a1 FTrue);
-       apply trueR
+       apply (ExchangeR ? a a1 FTrue);
+       apply TrueR
      ]
   ]
 qed.