(* File: Derivations.v  (last edited on 1/11/2000) (c) Klaus Weich  *)


Require Export Forms.


(*******   Derivations    *****************************************)

Inductive proof_term : Set :=
  | Var : nat -> proof_term
  | Efq : proof_term -> form -> proof_term
  | Abs : form -> proof_term -> proof_term
  | App : form -> proof_term -> proof_term -> proof_term
  | Pair : proof_term -> proof_term -> proof_term
  | PrL : form -> proof_term -> proof_term
  | PrR : form -> proof_term -> proof_term
  | OrFL : proof_term -> form -> proof_term
  | OrFR : proof_term -> form -> proof_term
  | Cas :
      form -> form -> proof_term -> proof_term -> proof_term -> proof_term
  | Shift : proof_term -> proof_term.



Inductive derives : flist -> proof_term -> form -> Prop :=
  | ByAssumption :
      forall (context : flist) (n : nat) (a : form),
      my_nth form n context a -> derives context (Var n) a
  | ByAbsurdity :
      forall (context : flist) (t : proof_term) (a : form),
      derives context t Falsum -> derives context (Efq t a) a
  | ImpIntro :
      forall (context : flist) (a : form) (r : proof_term) (b : form),
      derives (a :: context) r b -> derives context (Abs a r) (Imp a b)
  | ImpElim :
      forall (context : flist) (r s : proof_term) (a b : form),
      derives context r (Imp a b) ->
      derives context s a -> derives context (App a r s) b
  | AndFIntro :
      forall (context : flist) (r s : proof_term) (a b : form),
      derives context r a ->
      derives context s b -> derives context (Pair r s) (AndF a b)
  | AndFElimL :
      forall (context : flist) (r : proof_term) (a b : form),
      derives context r (AndF a b) -> derives context (PrL b r) a
  | AndFElimR :
      forall (context : flist) (r : proof_term) (a b : form),
      derives context r (AndF a b) -> derives context (PrR a r) b
  | OrFIntroL :
      forall (context : flist) (r : proof_term) (a b : form),
      derives context r a -> derives context (OrFL r b) (OrF a b)
  | OrFIntroR :
      forall (context : flist) (r : proof_term) (a b : form),
      derives context r b -> derives context (OrFR r a) (OrF a b)
  | OrFElim :
      forall (context : flist) (r s t : proof_term) (a b c : form),
      derives context r (OrF a b) ->
      derives (a :: context) s c ->
      derives (b :: context) t c -> derives context (Cas a b r s t) c
  | ShiftIntro :
      forall (context : flist) (r : proof_term) (a b : form),
      derives context r b -> derives (a :: context) (Shift r) b.


Lemma derives_rec :
 forall P : flist -> proof_term -> form -> Set,
 (forall (context : flist) (n : nat) (a : form),
  my_nth form n context a -> P context (Var n) a) ->
 (forall (context : flist) (t : proof_term) (a : form),
  derives context t Falsum -> P context t Falsum -> P context (Efq t a) a) ->
 (forall (context : flist) (a : form) (r : proof_term) (b : form),
  derives (a :: context) r b ->
  P (a :: context) r b -> P context (Abs a r) (Imp a b)) ->
 (forall (context : flist) (r s : proof_term) (a b : form),
  derives context r (Imp a b) ->
  P context r (Imp a b) ->
  derives context s a -> P context s a -> P context (App a r s) b) ->
 (forall (context : flist) (r s : proof_term) (a b : form),
  derives context r a ->
  P context r a ->
  derives context s b -> P context s b -> P context (Pair r s) (AndF a b)) ->
 (forall (context : flist) (r : proof_term) (a b : form),
  derives context r (AndF a b) ->
  P context r (AndF a b) -> P context (PrL b r) a) ->
 (forall (context : flist) (r : proof_term) (a b : form),
  derives context r (AndF a b) ->
  P context r (AndF a b) -> P context (PrR a r) b) ->
 (forall (context : flist) (r : proof_term) (a b : form),
  derives context r a -> P context r a -> P context (OrFL r b) (OrF a b)) ->
 (forall (context : flist) (r : proof_term) (a b : form),
  derives context r b -> P context r b -> P context (OrFR r a) (OrF a b)) ->
 (forall (context : flist) (r s t : proof_term) (a b c : form),
  derives context r (OrF a b) ->
  P context r (OrF a b) ->
  derives (a :: context) s c ->
  P (a :: context) s c ->
  derives (b :: context) t c ->
  P (b :: context) t c -> P context (Cas a b r s t) c) ->
 (forall (context : flist) (r : proof_term) (a b : form),
  derives context r b -> P context r b -> P (a :: context) (Shift r) b) ->
 forall (context : flist) (t : proof_term) (a : form),
 derives context t a -> P context t a.
(* Goal: forall (P : forall (_ : flist) (_ : proof_term) (_ : form), Set) (_ : forall (context : flist) (n : nat) (a : form) (_ : my_nth form n context a), P context (Var n) a) (_ : forall (context : flist) (t : proof_term) (a : form) (_ : derives context t Falsum) (_ : P context t Falsum), P context (Efq t a) a) (_ : forall (context : flist) (a : form) (r : proof_term) (b : form) (_ : derives (@cons form a context) r b) (_ : P (@cons form a context) r b), P context (Abs a r) (Imp a b)) (_ : forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : P context r (Imp a b)) (_ : derives context s a) (_ : P context s a), P context (App a r s) b) (_ : forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : P context r a) (_ : derives context s b) (_ : P context s b), P context (Pair r s) (AndF a b)) (_ : forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : P context r (AndF a b)), P context (PrL b r) a) (_ : forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : P context r (AndF a b)), P context (PrR a r) b) (_ : forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : P context r a), P context (OrFL r b) (OrF a b)) (_ : forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : P context r b), P context (OrFR r a) (OrF a b)) (_ : forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : P context r (OrF a b)) (_ : derives (@cons form a context) s c) (_ : P (@cons form a context) s c) (_ : derives (@cons form b context) t c) (_ : P (@cons form b context) t c), P context (Cas a b r s t) c) (_ : forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : P context r b), P (@cons form a context) (Shift r) b) (context : flist) (t : proof_term) (a : form) (_ : derives context t a), P context t a *)
intros P var efq abs app pari prl prr orl orr cas shift context t.
(* Goal: forall (a : form) (_ : derives context t a), P context t a *)
generalize context; clear context.
(* Goal: forall (context : flist) (a : form) (_ : derives context t a), P context t a *)
elim t; clear t.

(* Goal: forall (n : nat) (context : flist) (a : form) (_ : derives context (Var n) a), P context (Var n) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (Efq p f) a), P context (Efq p f) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros n context a der.
(* Goal: P context (Var n) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (Efq p f) a), P context (Efq p f) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply var.
(* Goal: derives context t a *)
inversion_clear der; assumption.

(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (Efq p f) a), P context (Efq p f) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros t ih a context b der.
(* Goal: P context (Efq t a) b *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
cut (a = b).
intros eq_a;  rewrite eq_a.
(* Goal: P context (Efq t b) b *)
(* Goal: @eq form a b *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply efq.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: @eq form a b0 *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der; trivial.

(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Abs f p) a), P context (Abs f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a t ih context b. 
(* Goal: forall _ : derives context (OrFR s a) b, P context (OrFR s a) b *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
case b; clear b.
(* Goal: forall _ : derives context (Abs a t) Falsum, P context (Abs a t) Falsum *)
(* Goal: forall (i : Int) (_ : derives context (Abs a t) (Atom i)), P context (Abs a t) (Atom i) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (AndF f f0)), P context (Abs a t) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (OrF f f0)), P context (Abs a t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (Imp f f0)), P context (Abs a t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros der_t; elimtype False; inversion_clear der_t.
(* Goal: forall (i : Int) (_ : derives context (Abs a t) (Atom i)), P context (Abs a t) (Atom i) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (AndF f f0)), P context (Abs a t) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (OrF f f0)), P context (Abs a t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (Imp f f0)), P context (Abs a t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros i der_t; elimtype False; inversion_clear der_t.
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (OrF f f0)), P context (Abs a t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (Imp f f0)), P context (Abs a t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der_t; elimtype False; inversion_clear der_t.
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (OrF f f0)), P context (Abs a t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (Imp f f0)), P context (Abs a t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der_t; elimtype False; inversion_clear der_t.
(* Goal: forall (f f0 : form) (_ : derives context (Abs a t) (Imp f f0)), P context (Abs a t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der_t.
(* Goal: P context (OrFR s a) (OrF b0 b1) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
cut (a = b0).
intros eq_a;  rewrite eq_a.
(* Goal: P context (Abs b0 t) (Imp b0 b1) *)
(* Goal: @eq form a b0 *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply abs.
(* Goal: derives (@cons form b0 context) t b1 *)
(* Goal: @eq form a b0 *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der_t; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives (@cons form b0 context) t b1 *)
(* Goal: @eq form a b0 *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der_t; assumption.
(* Goal: @eq form a b0 *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der_t; trivial.

(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (App f p p0) a), P context (App f p p0) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a s ih_s t ih_t context b der.
(* Goal: P context (App a s t) b *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply app.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form a context) s c *)
(* Goal: derives (@cons form b context) t c *)
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_s.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_t.
(* Goal: derives context t a *)
inversion_clear der; assumption.

(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (context : flist) (a : form) (_ : derives context (Pair p p0) a), P context (Pair p p0) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros s ih_s t ih_t context a.
(* Goal: forall _ : derives context (Pair s t) a, P context (Pair s t) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
case a; clear a.
(* Goal: forall _ : derives (@nil form) (Shift t) a, P (@nil form) (Shift t) a *)
(* Goal: forall (f : form) (l : list form) (_ : derives (@cons form f l) (Shift t) a), P (@cons form f l) (Shift t) a *)
intros der; elimtype False; inversion_clear der.
(* Goal: forall (i : Int) (_ : derives context (OrFR s a) (Atom i)), P context (OrFR s a) (Atom i) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (AndF f f0)), P context (OrFR s a) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (OrF f f0)), P context (OrFR s a) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros i der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (AndF f f0)), P context (Pair s t) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (OrF f f0)), P context (Pair s t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (Imp f f0)), P context (Pair s t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a0 a1 der.
(* Goal: P context (Pair s t) (AndF a0 a1) *)
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (OrF f f0)), P context (Pair s t) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (Imp f f0)), P context (Pair s t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply pari.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form a context) s c *)
(* Goal: derives (@cons form b context) t c *)
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_s.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_t.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (Imp f f0)), P context (Pair s t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a0 a1 der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (Pair s t) (Imp f f0)), P context (Pair s t) (Imp f f0) *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrL f p) a), P context (PrL f p) a *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a0 a1 der; elimtype False; inversion_clear der.

(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a s ih context b der.
(* Goal: P context (PrL a s) b *)
(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply prl.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.

(* Goal: forall (f : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (PrR f p) a), P context (PrR f p) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a s ih context b der.
(* Goal: P context (PrR a s) b *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFL p f) a), P context (OrFL p f) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply prr.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.

(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros s ih a context b.
(* Goal: forall _ : derives context (OrFR s a) b, P context (OrFR s a) b *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
case b; clear b.
(* Goal: forall _ : derives (@nil form) (Shift t) a, P (@nil form) (Shift t) a *)
(* Goal: forall (f : form) (l : list form) (_ : derives (@cons form f l) (Shift t) a), P (@cons form f l) (Shift t) a *)
intros der; elimtype False; inversion_clear der.
(* Goal: forall (i : Int) (_ : derives context (OrFR s a) (Atom i)), P context (OrFR s a) (Atom i) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (AndF f f0)), P context (OrFR s a) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (OrF f f0)), P context (OrFR s a) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros i der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (OrF f f0)), P context (OrFR s a) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der.
(* Goal: P context (OrFL s a) (OrF b0 b1) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFL s a) (Imp f f0)), P context (OrFL s a) (Imp f f0) *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
cut (a = b1).
intros eq_a;  rewrite eq_a.
(* Goal: P context (OrFL s b1) (OrF b0 b1) *)
(* Goal: @eq form a b1 *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFL s a) (Imp f f0)), P context (OrFL s a) (Imp f f0) *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply orl.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: @eq form a b0 *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der; trivial.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der; elimtype False; inversion_clear der.

(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (f : form) (context : flist) (a : form) (_ : derives context (OrFR p f) a), P context (OrFR p f) a *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros s ih a context b.
(* Goal: forall _ : derives context (OrFR s a) b, P context (OrFR s a) b *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
case b; clear b.
(* Goal: forall _ : derives (@nil form) (Shift t) a, P (@nil form) (Shift t) a *)
(* Goal: forall (f : form) (l : list form) (_ : derives (@cons form f l) (Shift t) a), P (@cons form f l) (Shift t) a *)
intros der; elimtype False; inversion_clear der.
(* Goal: forall (i : Int) (_ : derives context (OrFR s a) (Atom i)), P context (OrFR s a) (Atom i) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (AndF f f0)), P context (OrFR s a) (AndF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (OrF f f0)), P context (OrFR s a) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros i der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der; elimtype False; inversion_clear der.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (OrF f f0)), P context (OrFR s a) (OrF f f0) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der.
(* Goal: P context (OrFR s a) (OrF b0 b1) *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
cut (a = b0).
intros eq_a;  rewrite eq_a.
(* Goal: P context (OrFR s b0) (OrF b0 b1) *)
(* Goal: @eq form a b0 *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply orr.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: @eq form a b0 *)
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
inversion_clear der; trivial.
(* Goal: forall (f f0 : form) (_ : derives context (OrFR s a) (Imp f f0)), P context (OrFR s a) (Imp f f0) *)
(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros b0 b1 der; elimtype False; inversion_clear der.

(* Goal: forall (f f0 : form) (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (p0 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p0 a), P context p0 a) (p1 : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p1 a), P context p1 a) (context : flist) (a : form) (_ : derives context (Cas f f0 p p0 p1) a), P context (Cas f f0 p p0 p1) a *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros a b r ih_r s ih_s t ih_t context c der.
(* Goal: P context (Cas a b r s t) c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply cas.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context r (OrF a b) *)
(* Goal: derives (@cons form a context) s c *)
(* Goal: P (@cons form a context) s c *)
(* Goal: derives (@cons form b context) t c *)
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_r.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form a context) s c *)
(* Goal: derives (@cons form b context) t c *)
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_s.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P (@cons form b context) t c *)
(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
apply ih_t.
(* Goal: derives context t a *)
inversion_clear der; assumption.

(* Goal: forall (p : proof_term) (_ : forall (context : flist) (a : form) (_ : derives context p a), P context p a) (context : flist) (a : form) (_ : derives context (Shift p) a), P context (Shift p) a *)
intros t ih context a.
(* Goal: forall _ : derives context (Shift t) a, P context (Shift t) a *)
case context; clear context.
(* Goal: forall _ : derives (@nil form) (Shift t) a, P (@nil form) (Shift t) a *)
(* Goal: forall (f : form) (l : list form) (_ : derives (@cons form f l) (Shift t) a), P (@cons form f l) (Shift t) a *)
intros der; elimtype False; inversion_clear der.
(* Goal: forall (f : form) (l : list form) (_ : derives (@cons form f l) (Shift t) a), P (@cons form f l) (Shift t) a *)
intros b context der.
(* Goal: P (@cons form b context) (Shift t) a *)
apply shift.
(* Goal: derives context t a *)
inversion_clear der; assumption.
(* Goal: P context t a *)
apply ih.
(* Goal: derives context t a *)
inversion_clear der; assumption.
Qed.


