From 30e4cb7589afc0d4ef56ede52118269105377ea3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 14 Oct 2007 19:56:42 +0000 Subject: [PATCH] Caseness problems fixed. --- .../library/demo/propositional_sequent_calculus.ma | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma index 4498676a3..d79cd2e6d 100644 --- a/matita/library/demo/propositional_sequent_calculus.ma +++ b/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. -- 2.39.2