Commit 28fe2386 authored by Ulrich's avatar Ulrich

fixed the broken bottom rule

parent e7d3a2cf
......@@ -45,7 +45,7 @@ Inductive KIbox: form -> list form -> form -> Prop :=
| KIbox_impI G Z f1 f2: KIbox Z (f1 :: G) f2 -> KIbox Z G (f1 ->> f2)
| KIbox_boxIE G Z h F: (forall f, In f F -> KIbox Z G (|[]| f)) -> KIbox Z F h ->
KIbox Z G (|[]| h)
| KIbox_ffE G Z f: KIbox Z (ff :: G) f
| KIbox_ffE G Z f1 : KIbox Z G ff -> KIbox Z G f1
| KIbox_ttI G Z: KIbox Z G tt.
Hint Constructors KIbox : KIboxDB.
......
......@@ -84,10 +84,10 @@ Proof.
Qed.
Lemma ex_falso:
forall A G Z, KIbox Z G ff ->
forall G Z A, KIbox Z G ff ->
KIbox Z G A.
Proof.
eauto using KIbox_impE, KIbox_impI, KIbox_ffE.
exact KIbox_ffE.
Qed.
(** %\noindent% Tactic that proves the goal if its context contains [A] and [-! A]. *)
......@@ -98,8 +98,7 @@ Ltac context_contradiction A:= apply ex_falso; eapply ff_intro1 with A; intuitio
Lemma ex_falso_imp:
forall A G Z, KIbox Z G (ff ->> A).
Proof.
intros. apply KIbox_impI.
apply KIbox_ffE.
intros. eauto 3 with KIboxDB.
Qed.
(** * True *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment