Require Import Logic.lib.EnsemblesProperties.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.

Local Open Scope logic_base.

Section ContextProperty.

Context {L: Language}
        {minL: MinimunLanguage L}
        {Gamma: ProofTheory L}
        {fwSC: FiniteWitnessedSequentCalculus L Gamma}.

Lemma can_derive_finite_witnessed: forall x,
  finite_witnessed (can_derive x).
Proof.
(* Goal: forall x : @expr L, @finite_witnessed (@expr L) (@can_derive L Gamma x) *)
  intros; hnf; intros.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Phi xs) (@can_derive L Gamma x (fun x : @expr L => @In (@expr L) x xs))) *)
  apply derivable_finite_witnessed; auto.
Qed.

Lemma cannot_derive_finite_captured: forall x,
  finite_captured (cannot_derive x).
Proof.
(* Goal: forall x : @expr L, @finite_captured (@expr L) (@cannot_derive L Gamma x) *)
  intros.
(* Goal: @finite_captured (@expr L) (@cannot_derive L Gamma x) *)
  apply (not_finite_witnessed_finite_captured _ (can_derive_finite_witnessed x)).
Qed.

End ContextProperty.
