(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.

Require Import ILL.Definitions.

Require Import ill eill. 

Section EILL_ILL.

  Theorem EILL_ILL_PROVABILITY : EILL_PROVABILITY ⪯ ILL_PROVABILITY.
  Proof.
(* Goal: @reduces EILL_SEQUENT (prod (list ll_form) ll_form) EILL_PROVABILITY ILL_PROVABILITY *)
    exists (fun p => match p with (Si,Ga,p) => (map (fun c => ![i c]) Si ++ map £ Ga,£ p) end).
(* Goal: forall x : EILL_SEQUENT, iff (EILL_PROVABILITY x) (ILL_PROVABILITY (let (y, p) := x in let (Si, Ga) := y in @pair (list ll_form) ll_form (@app ll_form (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Si) (@map ill.ll_vars ll_form ll_var Ga)) (ll_var p))) *)
    intros ((Si,Ga),p); apply G_eill_correct.
  Qed.

End EILL_ILL.
