Caseness problems fixed.

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index 4498676a3ef10f8a793464138f94e2638e130730..d79cd2e6ddded90916b5a01f48d00d305dafd225 100644 (file)
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -752,18 +752,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.