Commit 7549380b authored by litak's avatar litak

fixed kuroda

parent 855d84d3
......@@ -477,7 +477,7 @@ Definition dneg_envelope (A : form) :=
forall Z, KIbox Z [] ((kol A) <<->> -+! (sub_vars_dneg A)).
Definition kuroda_envelope (Z : form) :=
forall A, KIbox Z [] ((kol A) <<->> -+! (sub_vars_dneg A)).
forall A, KIbox Z [] ((kol A) <<->> -+! A).
Corollary dneg_envelope_correct:
forall A, dneg_envelope A <-> pre_envelope A /\ post_envelope A.
......@@ -665,7 +665,7 @@ Proof.
rewrite adequate_eq_kol.
eapply eq_ded.
- eapply eq_sym. apply hip.
- eapply KIbox_impE. apply imp_dneg. apply KIbox_axiom.
- eapply KIbox_impE. apply imp_dneg. apply axiom_id.
Qed.
......@@ -787,7 +787,7 @@ Proof.
apply kuroda_envelope_adequate.
unfold kuroda_envelope.
induction A; unfold sub_vars_dneg in *; simpl.
- eapply eq_sym. apply eq_tneg.
- eapply eq_sym. apply eq_id. (*apply eq_tneg.*)
- eauto 4 with eq_impDB.
- eauto with eq_andDB.
- eauto with eq_orDB.
......
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