(* File: Kripke_Trees.v  (last edited on 25/10/2000) (c) Klaus Weich  *)


Require Export AvlTrees.
Require Export Trees.
Require Export Derivations.

(*******   Kripke_Model    ****************************************)


Inductive Kripke_Model (A : Set) (World : A -> Type) 
(le : A -> A -> Type) (forces0 : A -> Int -> Prop) : Type :=
    kripke_model :
      (forall k : A, World k -> le k k) ->
      (forall k0 k1 k2 : A,
       World k0 -> World k1 -> World k2 -> le k0 k1 -> le k1 k2 -> le k0 k2) ->
      (forall k0 k1 : A,
       World k0 ->
       World k1 -> le k0 k1 -> forall i : Int, forces0 k0 i -> forces0 k1 i) ->
      Kripke_Model A World le forces0.



Fixpoint forces (A : Set) (World : A -> Type) 
 (le : A -> A -> Type) (forces0 : A -> Int -> Prop) 
 (k : A) (a : form) {struct a} : Prop :=
  match a with
  | Falsum => False
  | Atom i => forces0 k i
  | AndF a0 a1 =>
      forces A World le forces0 k a0 /\ forces A World le forces0 k a1
  | OrF a0 a1 =>
      forces A World le forces0 k a0 \/ forces A World le forces0 k a1
  | Imp a0 a1 =>
      forall k' : A,
      World k' ->
      le k k' ->
      forces A World le forces0 k' a0 -> forces A World le forces0 k' a1
  end.


Lemma forces_mon :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall (k : A) (a : form),
 World k ->
 forces A World le forces0 k a ->
 forall k' : A, World k' -> le k k' -> forces A World le forces0 k' a.
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (a : form) (_ : World k) (_ : forces A World le forces0 k a) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' a *)
intros A World le forces0 kripke k a w; elim a; clear a.

(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (i : Int) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces0_t (Atms k') i) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces0_t (Atms k') i *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (AndF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
trivial.

(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: forces A World le forces0 k'' a1 *)
elim kripke.
(* Goal: forall (_ : forall (k : A) (_ : World k), le k k) (_ : forall (k0 k1 k2 : A) (_ : World k0) (_ : World k1) (_ : World k2) (_ : le k0 k1) (_ : le k1 k2), le k0 k2) (_ : forall (k0 k1 : A) (_ : World k0) (_ : World k1) (_ : le k0 k1) (i : Int) (_ : forces0 k0 i), forces0 k1 i), forces A World le forces0 k'' a1 *)
intros refl trans mon.
(* Goal: forces A World le forces0 k' (Atom i) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (AndF f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (OrF f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
simpl in |- *; apply (mon k k'); assumption.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (_ : and (forces A World le forces0 k a) (forces A World le forces0 k b)) (k' : A) (_ : World k') (_ : le k k'), and (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (OrF f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
intros u0; elim u0; clear u0; intros u0 u1.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), and (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (OrF f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
intros; split.
(* Goal: forces A World le forces0 k' a *)
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
apply ih_a; assumption.
(* Goal: forces A World le forces0 k' b *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
apply ih_b; assumption.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (_ : or (forces A World le forces0 k a) (forces A World le forces0 k b)) (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
intros u0; elim u0; clear u0; intros u0.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
intros; left.
(* Goal: forces A World le forces0 k' a *)
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
apply ih_a; assumption.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k'), or (forces A World le forces0 k' a) (forces A World le forces0 k' b) *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
intros; right.
(* Goal: forces A World le forces0 k' b *)
(* Goal: forall (f : form) (_ : forall (_ : forces A World le forces0 k f) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f) (f0 : form) (_ : forall (_ : forces A World le forces0 k f0) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' f0) (_ : forces A World le forces0 k (Imp f f0)) (k' : A) (_ : World k') (_ : le k k'), forces A World le forces0 k' (Imp f f0) *)
apply ih_b; assumption.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: forces A World le forces0 k'0 b *)
apply H.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forces A World le forces0 k'' a1 *)
elim kripke.
(* Goal: forall (_ : forall (k : A) (_ : World k), le k k) (_ : forall (k0 k1 k2 : A) (_ : World k0) (_ : World k1) (_ : World k2) (_ : le k0 k1) (_ : le k1 k2), le k0 k2) (_ : forall (k0 k1 : A) (_ : World k0) (_ : World k1) (_ : le k0 k1) (i : Int) (_ : forces0 k0 i), forces0 k1 i), forces A World le forces0 k'' a1 *)
intros refl trans mon.
(* Goal: Suc k'' k *)
apply (trans k k' k'0); assumption.
(* Goal: Suc k'' k *)
assumption.
Qed.



Lemma soundness :
 forall (t : proof_term) (context : flist) (a : form),
 derives context t a ->
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall k : A,
 World k ->
 (forall c : form, In c context -> forces A World le forces0 k c) ->
 forces A World le forces0 k a.
(* Goal: forall (t : proof_term) (context : flist) (a : form) (_ : derives context t a) (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
intros t context a der_t A World le forces0 kripke_model0.
(* Goal: forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
elim der_t; clear der_t t a context.

(* t=(Var n) *)
(* Goal: forall (context : flist) (n : nat) (a : form) (_ : my_nth form n context a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (t : proof_term) (a : form) (_ : derives context t Falsum) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k Falsum) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (a : form) (r : proof_term) (b : form) (_ : derives (@cons form a context) r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b) *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context n a nth k world forces_context.
(* Goal: forces A World le forces0 k c *)
apply forces_context.
(* Goal: Suc k'' k *)
apply nth_in with n; assumption.

(* t=(Efq r b) *)
(* Goal: forall (context : flist) (t : proof_term) (a : form) (_ : derives context t Falsum) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k Falsum) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (a : form) (r : proof_term) (b : form) (_ : derives (@cons form a context) r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b) *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a der_t ih k world forces_context.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k''' b *)
elimtype False.
(* Goal: forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih k world forces_context).

(* t=(Abs a0 r) *)
(* Goal: forall (context : flist) (a : form) (r : proof_term) (b : form) (_ : derives (@cons form a context) r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b) *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context a r b der_t ih k world forces_context.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a), forces A World le forces0 k' b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros k' world_k' le_k' forces_a0.
(* Goal: forces A World le forces0 k' b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih k' world_k').
(* Goal: forall (c : form) (_ : @In form c context), forces A World le forces0 k c *)
intros c in_c.
(* Goal: forces A World le forces0 k' c *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
inversion_clear in_c.
(* Goal: forces A World le forces0 k' c *)
(* Goal: forces A World le forces0 k' c *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r (Imp a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (Imp a b)) (_ : derives context s a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
 rewrite <- H.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
apply forces_mon with k; try assumption.
(* Goal: Suc k'' k *)
apply forces_context; assumption.

(* t=(App r s) *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r s a b der_r ih_r der_s ih_s k world forces_context.
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih_r k world forces_context k).
(* Goal: Suc k'' k *)
assumption.
(* Goal: le k k *)
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k a *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
elim kripke_model0; auto.
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih_s k world forces_context).

(* t=(Pair r s) *)
(* Goal: forall (context : flist) (r s : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (_ : derives context s b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r s a b der_r ih_r der_s ih_s k world forces_context.
(* Goal: and (forces_t2 k k' b0) (forces_t2 k k' b1) *)
split.
(* Goal: forces A World le forces0 k a *)
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih_r k world forces_context).
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r (AndF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (AndF a b)) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih_s k world forces_context).

(* t=(PrL r) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a b der_r ih k world forces_context.
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
generalize (ih k world forces_context).
(* Goal: Suc k'' k *)
intros u0; elim u0; intros; assumption.

(* t=(PrR r) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a b der_r ih k world forces_context.
(* Goal: forces A World le forces0 k b *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r a) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k a) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
generalize (ih k world forces_context).
(* Goal: Suc k'' k *)
intros u0; elim u0; intros; assumption.

(* t=(OrFL r b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a b der_r ih k world forces_context.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
left.
(* Goal: forces A World le forces0 k a *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k (OrF a b) *)
(* Goal: forall (context : flist) (r s t : proof_term) (a b c : form) (_ : derives context r (OrF a b)) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k (OrF a b)) (_ : derives (@cons form a context) s c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form a context)), forces A World le forces0 k c0), forces A World le forces0 k c) (_ : derives (@cons form b context) t c) (_ : forall (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 (@cons form b context)), forces A World le forces0 k c0), forces A World le forces0 k c) (k : A) (_ : World k) (_ : forall (c0 : form) (_ : @In form c0 context), forces A World le forces0 k c0), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply (ih k world forces_context).

(* t=(OrFR r b) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a b der_r ih k world forces_context.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
right.
(* Goal: Suc k'' k *)
apply ih; assumption.

(* t=(Cas r s t) *)
intros context r s t a b c der_r ih_r der_s ih_s der_t ih_t k world
 forces_context.
(* Goal: forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
generalize (ih_r k world forces_context); clear ih_r.
(* Goal: forall _ : forces A World le forces0 k (OrF a b), forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intro u0; elim u0; clear u0.
(* Goal: forall _ : forces A World le forces0 k' a0, forces A World le forces0 k' b *)
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
intro forces_a0.
(* Goal: forces A World le forces0 k c *)
(* Goal: forall _ : forces A World le forces0 k b, forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply ih_s; clear ih_s ih_t.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c *)
(* Goal: forall _ : forces A World le forces0 k b, forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros c0 in_c0.
(* Goal: forces A World le forces0 k c0 *)
(* Goal: forall _ : forces A World le forces0 k b, forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
inversion_clear in_c0.
(* Goal: Suc k'' k *)
 rewrite <- H; assumption.
(* Goal: Suc k'' k *)
apply forces_context; assumption.
(* Goal: forall _ : forces A World le forces0 k b, forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros forces_b.
(* Goal: forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
apply ih_t; clear ih_s ih_t.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forces A World le forces0 k c0 *)
(* Goal: forall _ : forces A World le forces0 k b, forces A World le forces0 k c *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros c0 in_c0; inversion_clear in_c0.
(* Goal: Suc k'' k *)
 rewrite <- H; assumption.
(* Goal: Suc k'' k *)
apply forces_context; assumption.

(* t=(Shift r) *)
(* Goal: forall (context : flist) (r : proof_term) (a b : form) (_ : derives context r b) (_ : forall (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c context), forces A World le forces0 k c), forces A World le forces0 k b) (k : A) (_ : World k) (_ : forall (c : form) (_ : @In form c (@cons form a context)), forces A World le forces0 k c), forces A World le forces0 k b *)
intros context r a b der_r ih k world forces_context.
(* Goal: forces_t k (vimp l (Imp (Atom i) b)) *)
apply ih.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forall (c : form) (_ : @In form c context), forces A World le forces0 k c *)
intros c in_c.
(* Goal: forces A World le forces0 k c *)
apply forces_context.
(* Goal: Suc k'' k *)
right; assumption.
Qed.



Lemma forces_b__forces_a_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall k : A,
 World k ->
 forall b : form,
 forces A World le forces0 k b ->
 forall a : form, forces A World le forces0 k (Imp a b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (_ : World k) (b : form) (_ : forces A World le forces0 k b) (a : form), forces A World le forces0 k (Imp a b) *)
intros A World le forces0 kripke k w b forces_b.
(* Goal: forall a : form, forces A World le forces0 k (Imp a b) *)
intros a.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a), forces A World le forces0 k' b *)
intros k' w' le_k_k' forces_a.
(* Goal: Suc k'' k *)
apply forces_mon with (k := k); assumption.
Qed.


Lemma forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall k : A,
 World k ->
 forall a0 a1 b : form,
 forces A World le forces0 k (Imp a0 (Imp a1 b)) ->
 forces A World le forces0 k (Imp (AndF a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (_ : World k) (a0 a1 b : form) (_ : forces A World le forces0 k (Imp a0 (Imp a1 b))), forces A World le forces0 k (Imp (AndF a0 a1) b) *)
intros A World le forces0 kripke k world a0 a1 b forces_a0_a1_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : and (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' u0 u1 forces_a0_and_a1.
(* Goal: forces A World le forces0 k' b *)
elim forces_a0_and_a1; clear forces_a0_and_a1.
(* Goal: forall (_ : forces A World le forces0 k' a0) (_ : forces A World le forces0 k' a1), forces A World le forces0 k' b *)
intros forces_a0 forces_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a0_a1_b k' u0 u1).
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a0 *)
(* Goal: World k' *)
(* Goal: le k' k' *)
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
apply forces_a0.
(* Goal: World k' *)
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
apply u0.
(* Goal: forces A World le forces0 k'' a1 *)
elim kripke.
(* Goal: forall (_ : forall (k : A) (_ : World k), le k k) (_ : forall (k0 k1 k2 : A) (_ : World k0) (_ : World k1) (_ : World k2) (_ : le k0 k1) (_ : le k1 k2), le k0 k2) (_ : forall (k0 k1 : A) (_ : World k0) (_ : World k1) (_ : le k0 k1) (i : Int) (_ : forces0 k0 i), forces0 k1 i), forces A World le forces0 k'' a1 *)
intros refl trans mon.
(* Goal: le k' k' *)
(* Goal: forces A World le forces0 k' a0 *)
apply refl.
(* Goal: World k' *)
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
apply u0.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
apply forces_a1.
Qed.


Lemma forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop) (k : A) (a0 a1 c b : form),
 forces A World le forces0 k (Imp a0 c) ->
 forces A World le forces0 k (Imp a1 c) ->
 forces A World le forces0 k (Imp c b) ->
 forces A World le forces0 k (Imp (OrF a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a0 a1 c b : form) (_ : forces A World le forces0 k (Imp a0 c)) (_ : forces A World le forces0 k (Imp a1 c)) (_ : forces A World le forces0 k (Imp c b)), forces A World le forces0 k (Imp (OrF a0 a1) b) *)
intros A World le forces0 k a0 a1 c b forces_a0_c forces_a1_c forces_c_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : or (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' u0 u1 forces_a0_or_a1.
(* Goal: forces A World le forces0 k' b *)
elim forces_a0_or_a1; clear forces_a0_or_a1.
(* Goal: forall _ : forces A World le forces0 k' a0, forces A World le forces0 k' b *)
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
intro forces_a0.
(* Goal: forces A World le forces0 k' b *)
apply (forces_c_b k' u0 u1).
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' c *)
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
apply (forces_a0_c k' u0 u1 forces_a0).
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
intro forces_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_c_b k' u0 u1).
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' c *)
apply (forces_a1_c k' u0 u1 forces_a1).
Qed.


Lemma forces_a0_imp_b_and_a1_imp_b__forces_a0_or_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop) (k : A) (a0 a1 b : form),
 forces A World le forces0 k (Imp a0 b) ->
 forces A World le forces0 k (Imp a1 b) ->
 forces A World le forces0 k (Imp (OrF a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a0 a1 b : form) (_ : forces A World le forces0 k (Imp a0 b)) (_ : forces A World le forces0 k (Imp a1 b)), forces A World le forces0 k (Imp (OrF a0 a1) b) *)
intros A World le forces0 k a0 a1 b forces_a0_b forces_a1_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : or (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' u0 u1 forces_a0_or_a1.
(* Goal: forces A World le forces0 k' b *)
elim forces_a0_or_a1; clear forces_a0_or_a1.
(* Goal: forall _ : forces A World le forces0 k' a0, forces A World le forces0 k' b *)
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
intro forces_a0.
(* Goal: forces A World le forces0 k' b *)
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
apply (forces_a0_b k' u0 u1 forces_a0).
(* Goal: forall _ : forces A World le forces0 k' a1, forces A World le forces0 k' b *)
intro forces_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a1_b k' u0 u1 forces_a1).
Qed.



Lemma forces_a1_imp_b__forces_a0_imp_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall k : A,
 World k ->
 forall a0 : form,
 forces A World le forces0 k a0 ->
 forall a1 b : form,
 forces A World le forces0 k (Imp a1 b) ->
 forces A World le forces0 k (Imp (Imp a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (_ : World k) (a0 : form) (_ : forces A World le forces0 k a0) (a1 b : form) (_ : forces A World le forces0 k (Imp a1 b)), forces A World le forces0 k (Imp (Imp a0 a1) b) *)
intros A World le forces0 kripke k w a0 forces_a0 a1 b forces_a1_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : and (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' w' le_k_k' forces_a0_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a1_b k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
change (forces A World le forces0 k' a1) in |- *.
(* Goal: forces A World le forces0 k' a1 *)
apply (forces_a0_a1 k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: forces A World le forces0 k'' a1 *)
elim kripke.
(* Goal: forall (_ : forall (k : A) (_ : World k), le k k) (_ : forall (k0 k1 k2 : A) (_ : World k0) (_ : World k1) (_ : World k2) (_ : le k0 k1) (_ : le k1 k2), le k0 k2) (_ : forall (k0 k1 : A) (_ : World k0) (_ : World k1) (_ : le k0 k1) (i : Int) (_ : forces0 k0 i), forces0 k1 i), forces A World le forces0 k'' a1 *)
intros refl trans mon.
(* Goal: le k' k' *)
(* Goal: forces A World le forces0 k' a0 *)
apply refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
apply forces_mon with (k := k); assumption.
Qed.

Lemma forces_a0_imp_a1_imp_b__forces_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop),
 Kripke_Model A World le forces0 ->
 forall k : A,
 World k ->
 forall a0 : form,
 forces A World le forces0 k a0 ->
 forall a1 b : form,
 forces A World le forces0 k (Imp (Imp a0 a1) b) ->
 forces A World le forces0 k (Imp a1 b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (_ : Kripke_Model A World le forces0) (k : A) (_ : World k) (a0 : form) (_ : forces A World le forces0 k a0) (a1 b : form) (_ : forces A World le forces0 k (Imp (Imp a0 a1) b)), forces A World le forces0 k (Imp a1 b) *)
intros A World le forces0 kripke k w a0 forces_a0 a1 b forces_a0a1_b.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a1), forces A World le forces0 k' b *)
intros k' w' le_k_k' forces_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a0a1_b k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forall (k'0 : A) (_ : World k'0) (_ : le k' k'0) (_ : (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k'0 a0), (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k'0 a1 *)
change (forces A World le forces0 k' (Imp a0 a1)) in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k'0 : A) (_ : World k'0) (_ : le k' k'0) (_ : forces A World le forces0 k'0 a0), forces A World le forces0 k'0 a1 *)
intros k'' w'' le'' forces_a0''.
(* Goal: forces A World le forces0 k'' a1 *)
elim kripke.
(* Goal: forall (_ : forall (k : A) (_ : World k), le k k) (_ : forall (k0 k1 k2 : A) (_ : World k0) (_ : World k1) (_ : World k2) (_ : le k0 k1) (_ : le k1 k2), le k0 k2) (_ : forall (k0 k1 : A) (_ : World k0) (_ : World k1) (_ : le k0 k1) (i : Int) (_ : forces0 k0 i), forces0 k1 i), forces A World le forces0 k'' a1 *)
intros refl trans mon.
(* Goal: Suc k'' k *)
apply forces_mon with (k := k'); assumption.
Qed.

Lemma forces_a0_imp_b__forces_a0_and_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop) (k : A) (a0 b : form),
 forces A World le forces0 k (Imp a0 b) ->
 forall a1 : form, forces A World le forces0 k (Imp (AndF a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a0 b : form) (_ : forces A World le forces0 k (Imp a0 b)) (a1 : form), forces A World le forces0 k (Imp (AndF a0 a1) b) *)
intros A World le forces0 k a0 b forces_a0_b a1.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : and (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' w' le_k_k' forces_a0_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a0_b k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a0 *)
change (forces A World le forces0 k' a0) in |- *.
(* Goal: forall (i : Int) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces0_t (Atms k') i) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces0_t (Atms k') i *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (AndF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
elim forces_a0_a1; trivial.
Qed.



Lemma forces_a1_imp_b__forces_a0_and_a1_imp_b :
 forall (A : Set) (World : A -> Type) (le : A -> A -> Type)
   (forces0 : A -> Int -> Prop) (k : A) (a1 b : form),
 forces A World le forces0 k (Imp a1 b) ->
 forall a0 : form, forces A World le forces0 k (Imp (AndF a0 a1) b).
(* Goal: forall (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a1 b : form) (_ : forces A World le forces0 k (Imp a1 b)) (a0 : form), forces A World le forces0 k (Imp (AndF a0 a1) b) *)
intros A World le forces0 k a1 b forces_a1_b a0.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : A) (_ : World k') (_ : le k k') (_ : and (forces A World le forces0 k' a0) (forces A World le forces0 k' a1)), forces A World le forces0 k' b *)
intros k' w' le_k_k' forces_a0_a1.
(* Goal: forces A World le forces0 k' b *)
apply (forces_a1_b k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) A World le forces0 k' a1 *)
change (forces A World le forces0 k' a1) in |- *.
(* Goal: forall (i : Int) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces0_t (Atms k') i) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces0_t (Atms k') i *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (AndF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
elim forces_a0_a1; trivial.
Qed.


(*******   kripke_trees    ****************************************)



Definition atoms := AVL unit.
Definition ANil := AVL_NIL unit.

Definition kripke_tree := Tree atoms.
Definition Kripke_Forest := Forest atoms.
Definition forces0_t (A : atoms) (i : Int) := LOOKUP unit i A tt.

Definition Is_Monotone_kripke_tree := Is_Monotone_Tree atoms Int forces0_t.
Definition Is_Monotone_Kripke_Forest :=
  Is_Monotone_Forest atoms Int forces0_t.

Definition Suc (k0 k1 : kripke_tree) := Successor atoms k0 k1.
Definition Atms (k : kripke_tree) := root atoms k.
Definition Succs (k0 : kripke_tree) := successors atoms k0.


Lemma kripke_tree_kripke_model :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k)
   (fun k0 k1 : kripke_tree => Suc k1 k0)
   (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i).
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
apply kripke_model.

(* Goal: forall (k0 k1 : kripke_tree) (_ : Suc k0 k) (_ : Suc k1 k) (_ : Suc k1 k0) (i : Int) (_ : forces0_t (Atms k0) i), forces0_t (Atms k1) i *)
unfold Suc in |- *.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply succs_refl.

(* Goal: forall (k0 k1 : kripke_tree) (_ : Suc k0 k) (_ : Suc k1 k) (_ : Suc k1 k0) (i : Int) (_ : forces0_t (Atms k0) i), forces0_t (Atms k1) i *)
unfold Suc in |- *.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: Suc k'' k *)
apply succs_trans with (t1 := k1); assumption.

(* Goal: forall (k0 k1 : kripke_tree) (_ : Suc k0 k) (_ : Suc k1 k) (_ : Suc k1 k0) (i : Int) (_ : forces0_t (Atms k0) i), forces0_t (Atms k1) i *)
unfold Suc in |- *.
(* Goal: forall (k0 k1 : kripke_tree) (_ : Successor atoms k0 k) (_ : Successor atoms k1 k) (_ : Successor atoms k1 k0) (i : Int) (_ : forces0_t (Atms k0) i), forces0_t (Atms k1) i *)
unfold Atms in |- *.
(* Goal: forall (k0 k1 : kripke_tree) (_ : Successor atoms k0 k) (_ : Successor atoms k1 k) (_ : Successor atoms k1 k0) (i : Int) (_ : forces0_t (root atoms k0) i), forces0_t (root atoms k1) i *)
intros k0 k1 suc0 suc1 suc1' i forces_k1.
(* Goal: forces0_t (root atoms k1) i *)
cut (Is_Monotone atoms Int forces0_t k).
(* Goal: forall _ : Is_Monotone atoms Int forces0_t k, forces0_t (root atoms k1) i *)
(* Goal: Is_Monotone atoms Int forces0_t k *)
intro is_mon_k.
(* Goal: forces0_t (root atoms k1) i *)
(* Goal: Is_Monotone atoms Int forces0_t k *)
inversion_clear is_mon_k.
(* Goal: Suc k'' k *)
apply H0 with (t0 := k0); assumption.
(* Goal: Is_Monotone atoms Int forces0_t k *)
apply is_monotone_tree_is_monotone.
(* Goal: Suc k'' k *)
assumption.
Qed.



Lemma kripke_tree_succ :
 forall K : kripke_tree,
 Is_Monotone_kripke_tree K ->
 forall k : kripke_tree, Suc k K -> Is_Monotone_kripke_tree k.
(* Goal: Is_Monotone_kripke_tree k' *)
(* Goal: Suc k' k' *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: forall (K : kripke_tree) (_ : Is_Monotone_Tree atoms Int forces0_t K) (k : kripke_tree) (_ : Suc k K), Is_Monotone_Tree atoms Int forces0_t k *)
intros K mon k suc.
(* Goal: Suc k'' k *)
apply is_monotone_tree_successor with K; assumption.
Qed.


Definition forces_t2 (K k : kripke_tree) (a : form) :=
  forces kripke_tree (fun k0 : kripke_tree => Suc k0 K)
    (fun k0 k1 : kripke_tree => Suc k1 k0)
    (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a.



Lemma forces_t2_is_local :
 forall (a : form) (k : kripke_tree),
 Is_Monotone_kripke_tree k ->
 forall k' : kripke_tree,
 Suc k' k ->
 forces_t2 k k' a ->
 forall K : kripke_tree,
 Is_Monotone_kripke_tree K -> Suc k' K -> forces_t2 K k' a.
(* Goal: forall (a : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' a *)
intros a; elim a; clear a.

(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forall (i : Int) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces0_t (Atms k') i) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces0_t (Atms k') i *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (AndF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
simpl in |- *; trivial.

(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (i : Int) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces0_t (Atms k') i) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces0_t (Atms k') i *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (AndF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
trivial.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b k mon_k k' suc_k'_k forces_k_k'_ab K mon_K suc_k'_K.
(* Goal: forces_t2 K k' (AndF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
elim forces_k_k'_ab.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' a) in |- *.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces_t2 k k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' b) in |- *.
(* Goal: forall (_ : forces_t2 k k' a) (_ : forces_t2 k k' b), forces_t2 K k' (AndF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
clear forces_k_k'_ab.
(* Goal: forall (_ : forces_t2 k k' a) (_ : forces_t2 k k' b), forces_t2 K k' (AndF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros u0 u1.
(* Goal: and (forces_t2 k k' b0) (forces_t2 k k' b1) *)
split.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
change (forces_t2 K k' a) in |- *.
(* Goal: Suc k'' k *)
apply ih_a with (k := k); assumption.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
change (forces_t2 K k' b) in |- *.
(* Goal: Suc k'' k *)
apply ih_b with (k := k); assumption.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b k mon_k k' suc_k'_k forces_k_k'_ab K mon_K suc_k'_K.
(* Goal: forall (_ : forces_t2 k k' a) (_ : forces_t2 k k' b), forces_t2 K k' (AndF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
elim forces_k_k'_ab; clear forces_k_k'_ab.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' a) in |- *.
(* Goal: forall _ : forces_t2 k k' a, forces_t2 K k' (OrF a b) *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intro u0.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
left.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
change (forces_t2 K k' a) in |- *.
(* Goal: Suc k'' k *)
apply ih_a with (k := k); assumption.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces_t2 k k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' b) in |- *.
(* Goal: forall _ : forces_t2 k k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros u0.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
right.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
change (forces_t2 K k' b) in |- *.
(* Goal: Suc k'' k *)
apply ih_b with (k := k); assumption.

(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros a ih_a b ih_b.
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp a b)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp a b) *)
intros k mon_k k' suc_k'_k forces_k_k'_ab K mon_K suc_k_K. 
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 K) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 b *)
intros k''.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' b *)
fold (forces_t2 K k'' a) in |- *.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 K) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' b *)
fold (forces_t2 K k'' b) in |- *.
(* Goal: forall (_ : Suc k'' K) (_ : Suc k'' k') (_ : forces_t2 K k'' a), forces_t2 K k'' b *)
intros.
(* Goal: forces_t2 K k'' b *)
apply ih_b with (k := k); clear ih_b.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
unfold Suc in |- *; apply succs_trans with k'; assumption.
(* Goal: forall (_ : forces_t2 k k' a) (_ : forces_t2 k k' b), forces_t2 K k' (AndF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (OrF f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
apply (forces_k_k'_ab k''); clear forces_k_k'_ab.
(* Goal: Suc k'' k *)
unfold Suc in |- *; apply succs_trans with k'; assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' a *)
(* Goal: Is_Monotone_kripke_tree K *)
(* Goal: Suc k'' K *)
change (forces_t2 k k'' a) in |- *.
(* Goal: forces_t2 k k'' a *)
(* Goal: Is_Monotone_kripke_tree K *)
(* Goal: Suc k'' K *)
apply ih_a with (k := K); clear ih_a.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
unfold Suc in |- *; apply succs_trans with k'; assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
Qed.



Definition forces_t (k : kripke_tree) := forces_t2 k k.


Lemma forces_t_imp :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall a b : form,
 (forces_t k a -> forces_t k b) ->
 (forall k' : kripke_tree,
  In_Forest atoms k' (Succs k) -> forces_t k' (Imp a b)) ->
 forces_t k (Imp a b).
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (a b : form) (_ : forall _ : forces_t k a, forces_t k b) (_ : forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs k)), forces_t k' (Imp a b)), forces_t k (Imp a b) *)
intros k mon a b forces_a_b foreach_succs.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k) (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
intro k'.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' a) in |- *.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces_t2 k k' a), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
fold (forces_t2 k k' b) in |- *.
(* Goal: forall (_ : Suc k' k) (_ : Suc k' k) (_ : forces_t2 k k' a), forces_t2 k k' b *)
intros suc_k'_k; clear suc_k'_k.
(* Goal: forall (_ : Suc k' k) (_ : forces_t2 k k' a), forces_t2 k k' b *)
intros suc_k'_k.
(* Goal: forall _ : forces_t2 k k' a, forces_t2 k k' b *)
inversion_clear suc_k'_k.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forall _ : forces_t2 k k' a, forces_t2 k k' b *)
intro forces_a.
(* Goal: forces_t2 k k' b *)
apply forces_t2_is_local with (k := t1).
(* Goal: Is_Monotone_kripke_tree k' *)
(* Goal: Suc k' k' *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: Is_Monotone_Tree atoms Int forces0_t k' *)
(* Goal: Suc k' k' *)
apply is_monotone_tree_successor with k. 
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 k *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply successor_trans with t1.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forces_t2 t1 k' b *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply (foreach_succs t1 H k').
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 t1) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
change (forces_t2 t1 k' a) in |- *.
(* Goal: forces_t2 k' k' a *)
apply forces_t2_is_local with (k := k).
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 k *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply successor_trans with t1.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Is_Monotone_kripke_tree k' *)
(* Goal: Suc k' k' *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: Is_Monotone_Tree atoms Int forces0_t k' *)
(* Goal: Suc k' k' *)
apply is_monotone_tree_successor with k.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 k *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply successor_trans with t1.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 k *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply successor_trans with t1.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
Qed.


Lemma forces_t_mon :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall a : form,
 forces_t k a -> forall k' : kripke_tree, Suc k' k -> forces_t k' a.
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (a : form) (_ : forces_t k a) (k' : kripke_tree) (_ : Suc k' k), forces_t k' a *)
intros k mon a forces_a k' suc.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k' k' a *)
apply forces_t2_is_local with (k := k).
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a *)
(* Goal: Is_Monotone_kripke_tree k' *)
(* Goal: Suc k' k' *)
apply forces_mon with (k := k).
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Is_Monotone_kripke_tree k' *)
(* Goal: Suc k' k' *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: Is_Monotone_Tree atoms Int forces0_t k' *)
(* Goal: Suc k' k' *)
apply is_monotone_tree_successor with k.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
Qed.



Lemma soundness_t :
 forall (t : proof_term) (context : flist) (a : form),
 derives context t a ->
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 (forall c : form, In c context -> forces_t k c) -> forces_t k a.
(* Goal: forall (t : proof_term) (context : flist) (a : form) (_ : derives context t a) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forall (c : form) (_ : @In form c context), forces_t k c), forces_t k a *)
intros t context a der_t k mon forces_context.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a *)
apply soundness with t context.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: forall (c : form) (_ : @In form c context), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k c *)
exact forces_context.
Qed.



Lemma forces_b__forces_a_imp_b_t :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall b : form, forces_t k b -> forall a : form, forces_t k (Imp a b).
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (b : form) (_ : forces_t k b) (a : form), forces_t k (Imp a b) *)
intros k mon b forces_b a.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
apply forces_b__forces_a_imp_b.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
Qed.


Lemma forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b_t :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall a0 a1 b : form,
 forces_t k (Imp a0 (Imp a1 b)) -> forces_t k (Imp (AndF a0 a1) b).
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (a0 a1 b : form) (_ : forces_t k (Imp a0 (Imp a1 b))), forces_t k (Imp (AndF a0 a1) b) *)
intros k mon a0 a1 b forces_a0_a1_b.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (AndF a0 a1) b) *)
apply forces_a0_imp_a1_imp_b__forces_a0_and_a1_imp_b.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
Qed.


Lemma forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b_t :
 forall (k : kripke_tree) (a0 a1 c b : form),
 forces_t k (Imp a0 c) ->
 forces_t k (Imp a1 c) ->
 forces_t k (Imp c b) -> forces_t k (Imp (OrF a0 a1) b).
(* Goal: forall (k : kripke_tree) (a0 a1 c b : form) (_ : forces_t k (Imp a0 c)) (_ : forces_t k (Imp a1 c)) (_ : forces_t k (Imp c b)), forces_t k (Imp (OrF a0 a1) b) *)
intros k a0 a1 c b forces_a0_c forces_a1_c forces_c_b.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
apply forces_a0_imp_c_and_a1_imp_c_and_c_imp_b__forces_a0_or_a1_imp_b with c;
(* Goal: Suc k'' k *)
 assumption.
Qed.


Lemma forces_a1_imp_b__forces_a0_imp_a1_imp_b_t :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall a0 : form,
 forces_t k a0 ->
 forall a1 b : form, forces_t k (Imp a1 b) -> forces_t k (Imp (Imp a0 a1) b).
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (a0 : form) (_ : forces_t k a0) (a1 b : form) (_ : forces_t k (Imp a1 b)), forces_t k (Imp (Imp a0 a1) b) *)
intros k mon a0 forces_a0 a1 b forces_a1_b.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply forces_a1_imp_b__forces_a0_imp_a1_imp_b.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
Qed.



Lemma forces_a0_imp_a1_imp_b__forces_a1_imp_b_t :
 forall k : kripke_tree,
 Is_Monotone_kripke_tree k ->
 forall a0 : form,
 forces_t k a0 ->
 forall a1 b : form, forces_t k (Imp (Imp a0 a1) b) -> forces_t k (Imp a1 b).
(* Goal: forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (a0 : form) (_ : forces_t k a0) (a1 b : form) (_ : forces_t k (Imp (Imp a0 a1) b)), forces_t k (Imp a1 b) *)
intros k mon a0 forces_a0 a1 b forces_a0a1_b.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a1 b) *)
apply forces_a0_imp_a1_imp_b__forces_a1_imp_b with a0.
(* Goal: Kripke_Model kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) *)
(* Goal: Suc k k *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k a0 *)
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (Imp a0 a1) b) *)
apply (kripke_tree_kripke_model k mon).
(* Goal: Successor atoms t1 t1 *)
(* Goal: Suc k' t1 *)
(* Goal: Is_Monotone_kripke_tree k *)
(* Goal: Suc k' k *)
unfold Suc in |- *; apply succs_refl.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
assumption.
Qed.


Lemma forces_a0_imp_b__forces_a0_and_a1_imp_b_t :
 forall (k : kripke_tree) (a0 b : form),
 forces_t k (Imp a0 b) -> forall a1 : form, forces_t k (Imp (AndF a0 a1) b).
(* Goal: forall (k : kripke_tree) (a0 b : form) (_ : forces_t k (Imp a0 b)) (a1 : form), forces_t k (Imp (AndF a0 a1) b) *)
intros k a0 b forces_a0_b a1.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (AndF a0 a1) b) *)
apply forces_a0_imp_b__forces_a0_and_a1_imp_b.
(* Goal: Suc k'' k *)
assumption.
Qed.



Lemma forces_a1_imp_b__forces_a0_and_a1_imp_b_t :
 forall (k : kripke_tree) (a1 b : form),
 forces_t k (Imp a1 b) -> forall a0 : form, forces_t k (Imp (AndF a0 a1) b).
(* Goal: forall (k : kripke_tree) (a1 b : form) (_ : forces_t k (Imp a1 b)) (a0 : form), forces_t k (Imp (AndF a0 a1) b) *)
intros k a1 b forces_a1_b a0.
(* Goal: forces_t k (Imp (AndF a0 a1) b) *)
unfold forces_t in |- *.
(* Goal: forces_t2 k k (Imp (AndF a0 a1) b) *)
unfold forces_t2 in |- *.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp (AndF a0 a1) b) *)
apply forces_a1_imp_b__forces_a0_and_a1_imp_b.
(* Goal: Suc k'' k *)
assumption.
Qed.


(*****************************************************************)

Lemma forces_a_a_imp_b__forces_b_t :
 forall (k : kripke_tree) (a b : form),
 forces_t k a -> forces_t k (Imp a b) -> forces_t k b.
(* Goal: forall (k : kripke_tree) (a b : form) (_ : forces_t k a) (_ : forces_t k (Imp a b)), forces_t k b *)
intros k a b forces_a forces_ab.
(* Goal: forces_t k b *)
apply (forces_ab k).
(* Goal: Suc k k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
unfold Suc in |- *; apply successor_refl.
(* Goal: Suc k k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
unfold Suc in |- *; apply successor_refl.
(* Goal: Suc k'' k *)
assumption.
Qed.


Lemma forces_a_imp_b0_a_imp_b1__forces_a_imp_a0_and_a1 :
 forall (a b0 b1 : form) (k : kripke_tree),
 forces_t k (Imp a b0) ->
 forces_t k (Imp a b1) -> forces_t k (Imp a (AndF b0 b1)).
(* Goal: forall (a b0 b1 : form) (k : kripke_tree) (_ : forces_t k (Imp a b0)) (_ : forces_t k (Imp a b1)), forces_t k (Imp a (AndF b0 b1)) *)
intros a b0 b1 k forces_ab0 forces_ab1.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k) (_ : forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), False), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' c *)
intros k' suc_k' suc_k''.
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a, and (forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b0) (forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b1) *)
change (forces_t2 k k' a -> forces_t2 k k' b0 /\ forces_t2 k k' b1) in |- *.
(* Goal: forall _ : forces_t2 k k' a, and (forces_t2 k k' b0) (forces_t2 k k' b1) *)
intros forces_a.
(* Goal: and (forces_t2 k k' b0) (forces_t2 k k' b1) *)
split.
(* Goal: Suc k'' k *)
apply (forces_ab0 k'); assumption.
(* Goal: Suc k'' k *)
apply (forces_ab1 k'); assumption.
Qed.


Lemma forces_a_imp_b__forces_a_imp_falsum_or_b :
 forall (k : kripke_tree) (a b : form),
 forces_t k (Imp a b) -> forces_t k (Imp a (OrF Falsum b)).
(* Goal: forall (k : kripke_tree) (a b : form) (_ : forces_t k (Imp a b)), forces_t k (Imp a (OrF b Falsum)) *)
intros k a b forces_ab.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k) (_ : forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), False), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' c *)
intros k' suc_k' suc_k''.
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a, or False (forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b) *)
change (forces_t2 k k' a -> False \/ forces_t2 k k' b) in |- *.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros forces_a; right.
(* Goal: Suc k'' k *)
apply (forces_ab k'); assumption.
Qed.


Lemma forces_a_imp_b__forces_a_imp_b_or_falsum :
 forall (k : kripke_tree) (a b : form),
 forces_t k (Imp a b) -> forces_t k (Imp a (OrF b Falsum)).
(* Goal: forall (k : kripke_tree) (a b : form) (_ : forces_t k (Imp a b)), forces_t k (Imp a (OrF b Falsum)) *)
intros k a b forces_ab.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k) (_ : forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), False), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' c *)
intros k' suc_k' suc_k''.
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a, or (forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b) False *)
change (forces_t2 k k' a -> forces_t2 k k' b \/ False) in |- *.
(* Goal: forces_t2 K k' (OrF a b) *)
(* Goal: forall _ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b, forces_t2 K k' (OrF a b) *)
(* Goal: forall (f : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f) (f0 : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' f0) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' f0) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp f f0)) (K : kripke_tree) (_ : Is_Monotone_kripke_tree K) (_ : Suc k' K), forces_t2 K k' (Imp f f0) *)
intros forces_a; left.
(* Goal: Suc k'' k *)
apply (forces_ab k'); assumption.
Qed.


Lemma forces_a_imp_falsum_imp_b1_t :
 forall (k : kripke_tree) (a b1 : form), forces_t k (Imp a (Imp Falsum b1)).
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: Suc k'' k *)
intros; elimtype False; assumption.
Qed.



Lemma forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c :
 forall (k : kripke_tree) (a b c : form),
 forces_t k (Imp (Imp a b) c) -> forces_t k (Imp (Imp a Falsum) c).
(* Goal: forall (k : kripke_tree) (a b c : form) (_ : forces_t k (Imp (Imp a b) c)), forces_t k (Imp (Imp a Falsum) c) *)
intros k a b c forces_abc.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k) (_ : forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), False), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' c *)
intros k' suc_k' suc_k''.
(* Goal: forall _ : forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), False, forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' c *)
change (forces_t2 k k' (Imp a Falsum) -> forces_t2 k k' c) in |- *.
(* Goal: forall _ : forces_t2 k k'' (Imp a Falsum), forces_t2 k k'' c *)
intros forces1.
(* Goal: Suc k'' k *)
apply (forces_abc k'); try assumption.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 a), (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 b *)
intros k'' suc3 suc4 forces_a.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k''' b *)
elimtype False.
(* Goal: Suc k'' k *)
apply (forces1 k''); assumption.
Qed.


Lemma forces_vimp :
 forall (k : kripke_tree) (l : list Int) (a b : form),
 (forall k' : kripke_tree, Suc k' k -> forces_t2 k k' a -> forces_t2 k k' b) ->
 forces_t k (vimp l a) -> forces_t k (vimp l b).
(* Goal: forall (k : kripke_tree) (l : list Int) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
intros k l.
(* Goal: forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
elim l; clear l.
(* Goal: forall (a b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a), forces_t2 k k' b) (_ : forces_t k (vimp (@nil Int) a)), forces_t k (vimp (@nil Int) b) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0), forces_t2 k k' b) (_ : forces_t k (vimp l a0)), forces_t k (vimp l b)) (a0 b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0), forces_t2 k k' b) (_ : forces_t k (vimp (@cons Int a l) a0)), forces_t k (vimp (@cons Int a l) b) *)
intros a b forces_ab forces_a.
(* Goal: Suc k'' k *)
apply forces_ab with (k' := k); try assumption.
(* Goal: Suc k k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
unfold Suc in |- *; apply successor_refl.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0), forces_t2 k k' b) (_ : forces_t k (vimp l a0)), forces_t k (vimp l b)) (a0 b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0), forces_t2 k k' b) (_ : forces_t k (vimp (@cons Int a l) a0)), forces_t k (vimp (@cons Int a l) b) *)
simpl in |- *; intros i l ih a b forces_ab forces_a.
(* Goal: Suc k'' k *)
apply ih with (a := Imp (Atom i) a); try assumption.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp (Atom i) a)), forces_t2 k k' (Imp (Atom i) b) *)
intros k' suc1 forces_ia.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces0_t (Atms k'0) i), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 b *)
intros k'' suc2 suc3 forces_i.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' b *)
change (forces_t2 k k'' b) in |- *.
(* Goal: forces_t2 k k'' b *)
apply forces_ab.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
apply (forces_ia k''); assumption.
Qed.


Lemma forces_vimp2 :
 forall (k : kripke_tree) (l : list Int) (a b c : form),
 (forall k' : kripke_tree,
  Suc k' k -> forces_t2 k k' a -> forces_t2 k k' b -> forces_t2 k k' c) ->
 forces_t k (vimp l a) -> forces_t k (vimp l b) -> forces_t k (vimp l c).
(* Goal: forall (k : kripke_tree) (l : list Int) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
intros k l.
(* Goal: forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
elim l; clear l.
(* Goal: forall (a b c : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a) (_ : forces_t2 k k' b), forces_t2 k k' c) (_ : forces_t k (vimp (@nil Int) a)) (_ : forces_t k (vimp (@nil Int) b)), forces_t k (vimp (@nil Int) c) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b c : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0) (_ : forces_t2 k k' b), forces_t2 k k' c) (_ : forces_t k (vimp l a0)) (_ : forces_t k (vimp l b)), forces_t k (vimp l c)) (a0 b c : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0) (_ : forces_t2 k k' b), forces_t2 k k' c) (_ : forces_t k (vimp (@cons Int a l) a0)) (_ : forces_t k (vimp (@cons Int a l) b)), forces_t k (vimp (@cons Int a l) c) *)
intros a b c forces_abc forces_a forces_b.
(* Goal: Suc k'' k *)
apply forces_abc with (k' := k); try assumption.
(* Goal: Suc k k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
unfold Suc in |- *; apply successor_refl.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b c : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0) (_ : forces_t2 k k' b), forces_t2 k k' c) (_ : forces_t k (vimp l a0)) (_ : forces_t k (vimp l b)), forces_t k (vimp l c)) (a0 b c : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' a0) (_ : forces_t2 k k' b), forces_t2 k k' c) (_ : forces_t k (vimp (@cons Int a l) a0)) (_ : forces_t k (vimp (@cons Int a l) b)), forces_t k (vimp (@cons Int a l) c) *)
simpl in |- *; intros i l ih a b c forces_abc forces_a forces_b.
(* Goal: Suc k'' k *)
apply ih with (a := Imp (Atom i) a) (b := Imp (Atom i) b); try assumption.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : forces_t2 k k' (Imp (Atom i) a)) (_ : forces_t2 k k' (Imp (Atom i) b)), forces_t2 k k' (Imp (Atom i) c) *)
intros k' suc1 forces_ia forces_ib.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces0_t (Atms k'0) i), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 b *)
intros k'' suc2 suc3 forces_i.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' c *)
change (forces_t2 k k'' c) in |- *.
(* Goal: forces_t2 k k'' c *)
apply forces_abc.
(* Goal: Suc k'' k *)
assumption.
(* Goal: Suc k'' k *)
apply (forces_ia k''); assumption.
(* Goal: Suc k'' k *)
apply (forces_ib k''); assumption.
Qed.




Lemma forces_vimp0 :
 forall (k : kripke_tree) (l : list Int) (b : form),
 (forall k' : kripke_tree, Suc k' k -> forces_t2 k k' b) ->
 forces_t k (vimp l b).
(* Goal: forall (k : kripke_tree) (l : list Int) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
intros k l.
(* Goal: forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b) *)
elim l; clear l.
(* Goal: forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@nil Int) b) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
intros b forces_ab.
(* Goal: Suc k'' k *)
apply forces_ab with (k' := k); try assumption.
(* Goal: Suc k k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
unfold Suc in |- *; apply successor_refl.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp l b)) (b : form) (_ : forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' b), forces_t k (vimp (@cons Int a l) b) *)
simpl in |- *; intros i l ih b forces_ab.
(* Goal: forces_t k (vimp l (Imp (Atom i) b)) *)
apply ih.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k), forces_t2 k k' (Imp (Atom i) b) *)
intros k' suc1.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forces0_t (Atms k'0) i), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 b *)
intros k'' suc2 suc3 forces_i.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' b *)
change (forces_t2 k k'' b) in |- *.
(* Goal: forces_t2 k k'' b *)
apply forces_ab.
(* Goal: Suc k'' k *)
assumption.
Qed.



Lemma forces_a_imp_b_imp_c__forces_a_imp_falsum_imp_c_t2 :
 forall (k k' : kripke_tree) (a b c : form),
 Suc k' k ->
 forces_t2 k k' (Imp (Imp a b) c) -> forces_t2 k k' (Imp (Imp a Falsum) c).
(* Goal: forall (k k' : kripke_tree) (a b c : form) (_ : Suc k' k) (_ : forces_t2 k k' (Imp (Imp a b) c)), forces_t2 k k' (Imp (Imp a Falsum) c) *)
intros k k' a b c suc1 forces_abc.
(* Goal: forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k (Imp a b) *)
unfold forces_t in |- *; unfold forces_t2 in |- *; simpl in |- *.
(* Goal: forall (k'0 : kripke_tree) (_ : Suc k'0 k) (_ : Suc k'0 k') (_ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k'0) (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), False), forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'0 c *)
intros k'' suc_k' suc_k''.
(* Goal: forall _ : forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k'') (_ : forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), False, forces kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k'' c *)
change (forces_t2 k k'' (Imp a Falsum) -> forces_t2 k k'' c) in |- *.
(* Goal: forall _ : forces_t2 k k'' (Imp a Falsum), forces_t2 k k'' c *)
intros forces1.
(* Goal: Suc k'' k *)
apply (forces_abc k''); try assumption.
(* Goal: forall (k' : kripke_tree) (_ : Suc k' k) (_ : Suc k' k'') (_ : (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k'0 : A) (_ : World k'0) (_ : le k k'0) (_ : forces A World le forces0 k'0 a0), forces A World le forces0 k'0 a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' a), (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k'0 : A) (_ : World k'0) (_ : le k k'0) (_ : forces A World le forces0 k'0 a0), forces A World le forces0 k'0 a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k' b *)
intros k''' suc3 suc4 forces_a.
(* Goal: (fix forces (A : Set) (World : forall _ : A, Type) (le : forall (_ : A) (_ : A), Type) (forces0 : forall (_ : A) (_ : Int), Prop) (k : A) (a : form) {struct a} : Prop := match a with | Falsum => False | Atom i => forces0 k i | AndF a0 a1 => and (forces A World le forces0 k a0) (forces A World le forces0 k a1) | OrF a0 a1 => or (forces A World le forces0 k a0) (forces A World le forces0 k a1) | Imp a0 a1 => forall (k' : A) (_ : World k') (_ : le k k') (_ : forces A World le forces0 k' a0), forces A World le forces0 k' a1 end) kripke_tree (fun k0 : kripke_tree => Suc k0 k) (fun k0 k1 : kripke_tree => Suc k1 k0) (fun (k0 : kripke_tree) (i : Int) => forces0_t (Atms k0) i) k''' b *)
elimtype False.
(* Goal: Suc k'' k *)
apply (forces1 k'''); assumption.
Qed.
