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

Require Export ML_Int.
Require Export My_Nth.

(*******   forms    ***********************************************)

Inductive form : Set :=
  | Falsum : form
  | Atom : Int -> form
  | AndF : form -> form -> form
  | OrF : form -> form -> form
  | Imp : form -> form -> form.

Definition flist := list form.
Definition fnil := nil (A:=form).


(* vimp qs a := vec(qs) imp a *)

Fixpoint vimp (qs : list Int) : form -> form :=
  match qs with
  | nil => fun a : form => a
  | q :: qs => fun a : form => vimp qs (Imp (Atom q) a)
  end.



(*********************************************************************)
(* Substitute (Atom i) by a in b:                                    *)


Fixpoint subst_form (i : Int) (a b : form) {struct b} : form :=
  match b with
  | Falsum => Falsum
  | Atom j => match equal_dec i j with
              | left _ => a
              | right _ => Atom j
              end
  | OrF b0 b1 => OrF (subst_form i a b0) (subst_form i a b1)
  | AndF b0 b1 => AndF (subst_form i a b0) (subst_form i a b1)
  | Imp b0 b1 => Imp (subst_form i a b0) (subst_form i a b1)
  end.


Definition subst_list (i : Int) (a : form) (l : flist) :=
  map (subst_form i a) l.



Lemma subst_nth :
 forall (i : Int) (g : form) (n : nat) (l : flist) (a : form),
 my_nth form n l a -> my_nth form n (subst_list i g l) (subst_form i g a).
(* Goal: forall (i : Int) (g : form) (n : nat) (l : flist) (a : form) (_ : my_nth form n l a), my_nth form n (subst_list i g l) (subst_form i g a) *)
intros i g n; elim n; clear n.
(* Goal: forall (l : flist) (a : form) (_ : my_nth form O l a), my_nth form O (subst_list i g l) (subst_form i g a) *)
(* Goal: forall (n : nat) (_ : forall (l : flist) (a : form) (_ : my_nth form n l a), my_nth form n (subst_list i g l) (subst_form i g a)) (l : flist) (a : form) (_ : my_nth form (S n) l a), my_nth form (S n) (subst_list i g l) (subst_form i g a) *)
intros l a nth; inversion_clear nth.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: my_nth form O (@cons form (subst_form i g a) (subst_list i g l0)) (subst_form i g a) *)
(* Goal: forall (n : nat) (_ : forall (l : flist) (a : form) (_ : my_nth form n l a), my_nth form n (subst_list i g l) (subst_form i g a)) (l : flist) (a : form) (_ : my_nth form (S n) l a), my_nth form (S n) (subst_list i g l) (subst_form i g a) *)
apply My_NthO.

(* Goal: forall (n : nat) (_ : forall (l : flist) (a : form) (_ : my_nth form n l a), my_nth form n (subst_list i g l) (subst_form i g a)) (l : flist) (a : form) (_ : my_nth form (S n) l a), my_nth form (S n) (subst_list i g l) (subst_form i g a) *)
intros n ih l a nth.
(* Goal: my_nth form (S n) (subst_list i g l) (subst_form i g a) *)
inversion_clear nth.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: my_nth form (S n) (@cons form (subst_form i g a0) (subst_list i g l0)) (subst_form i g a) *)
apply My_NthS.
(* Goal: my_nth form n (subst_list i g l0) (subst_form i g a) *)
apply ih.
(* Goal: below_form a j *)
assumption.
Qed.


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

Fixpoint below_form (a : form) (i : Int) {struct a} : Prop :=
  match a with
  | Falsum => True
  | Atom j => Less j i
  | AndF a0 a1 => below_form a0 i /\ below_form a1 i
  | OrF a0 a1 => below_form a0 i /\ below_form a1 i
  | Imp a0 a1 => below_form a0 i /\ below_form a1 i
  end.

Definition below_list (L : flist) (i : Int) :=
  forall a : form, In a L -> below_form a i.


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


Lemma below_form_less_below_form :
 forall (a : form) (i j : Int), below_form a i -> Less i j -> below_form a j.
(* Goal: forall (a : form) (i j : Int) (_ : below_form a i) (_ : Less i j), below_form a j *)
intros a i j.
(* Goal: forall (_ : below_form a i) (_ : Less i j), below_form a j *)
elim a; clear a.
(* Goal: forall (b : form) (_ : forall (i : Int) (_ : @In Int i (@nil Int)), Less i j), @eq form (subst_form j a (vimp (@nil Int) b)) (vimp (@nil Int) (subst_form j a b)) *)
(* Goal: forall (a0 : Int) (l : list Int) (_ : forall (b : form) (_ : forall (i : Int) (_ : @In Int i l), Less i j), @eq form (subst_form j a (vimp l b)) (vimp l (subst_form j a b))) (b : form) (_ : forall (i : Int) (_ : @In Int i (@cons Int a0 l)), Less i j), @eq form (subst_form j a (vimp (@cons Int a0 l) b)) (vimp (@cons Int a0 l) (subst_form j a b)) *)
intros; trivial.

(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: forall (i0 : Int) (_ : Less i0 i) (_ : Less i j), Less i0 j *)
(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (AndF f f0) i) (_ : Less i j), below_form (AndF f f0) j *)
(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (OrF f f0) i) (_ : Less i j), below_form (OrF f f0) j *)
(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (Imp f f0) i) (_ : Less i j), below_form (Imp f f0) j *)
intros i0 less_i0 less_i.
(* Goal: below_form a j *)
apply less_trans with i; assumption.

(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (Imp f f0) i) (_ : Less i j), below_form (Imp f f0) j *)
intros a ih_a b ih_b below_ab less_ij.
(* Goal: below_form (Imp a b) j *)
elim below_ab; clear below_ab.
(* Goal: forall (_ : below_form a i) (_ : below_form b i), below_form (Imp a b) j *)
intros below_a below_b.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
apply ih_a; assumption.
(* Goal: below_form a j *)
apply ih_b; assumption.

(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (Imp f f0) i) (_ : Less i j), below_form (Imp f f0) j *)
intros a ih_a b ih_b below_ab less_ij.
(* Goal: below_form (Imp a b) j *)
elim below_ab; clear below_ab.
(* Goal: forall (_ : below_form a i) (_ : below_form b i), below_form (Imp a b) j *)
intros below_a below_b.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
apply ih_a; assumption.
(* Goal: below_form a j *)
apply ih_b; assumption.

(* Goal: forall (f : form) (_ : forall (_ : below_form f i) (_ : Less i j), below_form f j) (f0 : form) (_ : forall (_ : below_form f0 i) (_ : Less i j), below_form f0 j) (_ : below_form (Imp f f0) i) (_ : Less i j), below_form (Imp f f0) j *)
intros a ih_a b ih_b below_ab less_ij.
(* Goal: below_form (Imp a b) j *)
elim below_ab; clear below_ab.
(* Goal: forall (_ : below_form a i) (_ : below_form b i), below_form (Imp a b) j *)
intros below_a below_b.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
apply ih_a; assumption.
(* Goal: below_form a j *)
apply ih_b; assumption.
Qed.




Lemma below_list_less_below_list :
 forall (l : flist) (i j : Int), below_list l i -> Less i j -> below_list l j.
(* Goal: forall (l : flist) (i j : Int) (_ : below_list l i) (_ : Less i j), below_list l j *)
intros l i j below_l less_ij.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a : form) (_ : @In form a l), below_form a j *)
intros a in_a.
(* Goal: below_form a j *)
apply below_form_less_below_form with i.
(* Goal: below_form a j *)
apply below_l; assumption.
(* Goal: below_form a j *)
assumption.
Qed.


Lemma below_cons_list_head :
 forall (a : form) (l : flist) (i : Int),
 below_list (a :: l) i -> below_form a i.
(* Goal: forall (a : form) (l : flist) (i : Int) (_ : below_list (@cons form a l) i), below_list l i *)
intros a l i below_l.
(* Goal: Less i0 j *)
apply below_l. 
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
Qed.


Lemma below_cons_list_tail :
 forall (a : form) (l : flist) (i : Int),
 below_list (a :: l) i -> below_list l i.
(* Goal: forall (a : form) (l : flist) (i : Int) (_ : below_list (@cons form a l) i), below_list l i *)
intros a l i below_l.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a0 : form) (_ : @In form a0 (@cons form a l)), below_form a0 i *)
intros b in_b.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: below_form a j *)
right; assumption.
Qed.

Lemma below_cons_list :
 forall (a : form) (l : flist) (i : Int),
 below_form a i -> below_list l i -> below_list (a :: l) i.
(* Goal: forall (a : form) (l : flist) (i : Int) (_ : below_form a i) (_ : below_list l i), below_list (@cons form a l) i *)
intros a l i below_a below_l.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a0 : form) (_ : @In form a0 (@cons form a l)), below_form a0 i *)
intros b in_b.
(* Goal: below_form b i *)
inversion_clear in_b.
(* Goal: below_form a j *)
 rewrite <- H; assumption.
(* Goal: below_form a j *)
apply below_l; assumption.
Qed.


Lemma below_list_weak :
 forall (l : flist) (a b : form) (i : Int),
 (below_form a i -> below_form b i) ->
 below_list (a :: l) i -> below_list (b :: l) i.
(* Goal: forall (l : flist) (a b : form) (i : Int) (_ : forall _ : below_form a i, below_form b i) (_ : below_list (@cons form a l) i), below_list (@cons form b l) i *)
intros l a b i below_ab below_l.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a : form) (_ : @In form a (@cons form b (@cons form c l))), below_form a i *)
(* Goal: below_form a i *)
intros x in_x.
(* Goal: below_form x i *)
(* Goal: below_form a i *)
inversion_clear in_x.
(* Goal: below_form x i *)
(* Goal: below_form x i *)
 rewrite <- H; clear H x.
(* Goal: below_form b i *)
(* Goal: below_form x i *)
apply below_ab.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: below_form a j *)
right; assumption.
Qed.



Lemma below_list_weak2 :
 forall (l : flist) (a b c : form) (i : Int),
 (below_form a i -> below_form b i /\ below_form c i) ->
 below_list (a :: l) i -> below_list (b :: c :: l) i.
(* Goal: forall (l : flist) (a b c : form) (i : Int) (_ : forall _ : below_form a i, and (below_form b i) (below_form c i)) (_ : below_list (@cons form a l) i), below_list (@cons form b (@cons form c l)) i *)
intros l a b c i below_abc below_l.
(* Goal: below_list (@cons form b (@cons form c l)) i *)
elim below_abc; clear below_abc.
(* Goal: forall (_ : below_form b i) (_ : below_form c i), below_list (@cons form b (@cons form c l)) i *)
(* Goal: below_form a i *)
intros below_b below_c.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a : form) (_ : @In form a (@cons form b (@cons form c l))), below_form a i *)
(* Goal: below_form a i *)
intros x in_x.
(* Goal: below_form x i *)
(* Goal: below_form a i *)
inversion_clear in_x.
(* Goal: below_form a j *)
 rewrite <- H; assumption.
(* Goal: below_form x i *)
(* Goal: below_form a i *)
inversion_clear H.
(* Goal: below_form a j *)
 rewrite <- H0; assumption.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: below_form a j *)
right; assumption.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
Qed.


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


Lemma subst_form_below :
 forall (i : Int) (g a : form), below_form a i -> subst_form i g a = a.
(* Goal: forall (_ : below_form a i) (_ : Less i j), below_form a j *)
intros i g a; elim a; clear a.

(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.

(* Goal: forall (i0 : Int) (_ : below_form (Atom i0) i), @eq form (subst_form i g (Atom i0)) (Atom i0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
intros j.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: forall _ : Less j i, @eq form (if equal_dec i j then g else Atom j) (Atom j) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
intros less_j.
(* Goal: @eq form (if equal_dec i j then g else Atom j) (Atom j) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
elim (equal_dec i j).
(* Goal: forall _ : Equal i j, @eq form g (Atom j) *)
(* Goal: forall _ : not (Equal i j), @eq form (Atom j) (Atom j) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
intros equal_j.
(* Goal: @eq form g (Atom j) *)
(* Goal: forall _ : not (Equal i j), @eq form (Atom j) (Atom j) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
elimtype False.
(* Goal: False *)
(* Goal: forall _ : not (Equal i j), @eq form (Atom j) (Atom j) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (AndF f f0) i), @eq form (subst_form i g (AndF f f0)) (AndF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (OrF f f0) i), @eq form (subst_form i g (OrF f f0)) (OrF f f0) *)
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : below_form (Imp f f0) i), @eq form (subst_form i g (Imp f f0)) (Imp f f0) *)
apply less_irrefl with i.
(* Goal: below_form a j *)
apply equal_less_less with j; assumption.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.

(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : and (below_form f i) (below_form f0 i)), @eq form (Imp (subst_form i g f) (subst_form i g f0)) (Imp f f0) *)
intros a ih_a b ih_b below_ab.
(* Goal: @eq form (Imp (subst_form i g a) (subst_form i g b)) (Imp a b) *)
 rewrite ih_a.
(* Goal: @eq form (Imp a (subst_form i g b)) (Imp a b) *)
(* Goal: below_form a i *)
 rewrite ih_b.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.

(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : and (below_form f i) (below_form f0 i)), @eq form (Imp (subst_form i g f) (subst_form i g f0)) (Imp f f0) *)
intros a ih_a b ih_b below_ab.
(* Goal: @eq form (Imp (subst_form i g a) (subst_form i g b)) (Imp a b) *)
 rewrite ih_a.
(* Goal: @eq form (Imp a (subst_form i g b)) (Imp a b) *)
(* Goal: below_form a i *)
 rewrite ih_b.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.

(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: forall (f : form) (_ : forall _ : below_form f i, @eq form (subst_form i g f) f) (f0 : form) (_ : forall _ : below_form f0 i, @eq form (subst_form i g f0) f0) (_ : and (below_form f i) (below_form f0 i)), @eq form (Imp (subst_form i g f) (subst_form i g f0)) (Imp f f0) *)
intros a ih_a b ih_b below_ab.
(* Goal: @eq form (Imp (subst_form i g a) (subst_form i g b)) (Imp a b) *)
 rewrite ih_a.
(* Goal: @eq form (Imp a (subst_form i g b)) (Imp a b) *)
(* Goal: below_form a i *)
 rewrite ih_b.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
elim below_ab; trivial.
Qed.


Lemma subst_list_below :
 forall (i : Int) (g : form) (l : flist),
 below_list l i -> subst_list i g l = l.
(* Goal: forall (i : Int) (g : form) (l : flist) (_ : below_list l i), @eq (list form) (subst_list i g l) l *)
intros i g l; elim l; clear l.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.

(* Goal: forall (a : form) (l : list form) (_ : forall _ : below_list l i, @eq (list form) (subst_list i g l) l) (_ : below_list (@cons form a l) i), @eq (list form) (subst_list i g (@cons form a l)) (@cons form a l) *)
simpl in |- *; intros a l ih below_l.
(* Goal: @eq (list form) (@cons form (subst_form i g a) (subst_list i g l)) (@cons form a l) *)
 rewrite ih.
(* Goal: @eq (list form) (@cons form (subst_form i g a) l) (@cons form a l) *)
(* Goal: below_list l i *)
 rewrite (subst_form_below i g a).
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.
(* Goal: below_form a i *)
(* Goal: below_list l i *)
apply (below_l a).
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
(* Goal: below_list l i *)
unfold below_list in |- *.
(* Goal: forall (a : form) (_ : @In form a l), below_form a i *)
intros b in_l.
(* Goal: below_form b i *)
apply (below_l b).
(* Goal: below_form a j *)
right; assumption.
Qed.



Lemma below_vimp :
 forall (j : Int) (l : list Int) (a b : form),
 (forall j : Int, below_form a j -> below_form b j) ->
 below_form (vimp l a) j -> below_form (vimp l b) j.
(* Goal: forall (j : Int) (l : list Int) (a b : form) (_ : forall (j0 : Int) (_ : below_form a j0), below_form b j0) (_ : below_form (vimp l a) j), below_form (vimp l b) j *)
intros j l.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
elim l; clear l.
(* Goal: forall (a b : form) (_ : forall (j : Int) (_ : below_form a j), below_form b j) (_ : below_form (vimp (@nil Int) a) j), below_form (vimp (@nil Int) b) j *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b : form) (_ : forall (j : Int) (_ : below_form a0 j), below_form b j) (_ : below_form (vimp l a0) j), below_form (vimp l b) j) (a0 b : form) (_ : forall (j : Int) (_ : below_form a0 j), below_form b j) (_ : below_form (vimp (@cons Int a l) a0) j), below_form (vimp (@cons Int a l) b) j *)
intros a b below_ab below_a.
(* Goal: below_form a j *)
apply below_ab; assumption.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b : form) (_ : forall (j : Int) (_ : below_form a0 j), below_form b j) (_ : below_form (vimp l a0) j), below_form (vimp l b) j) (a0 b : form) (_ : forall (j : Int) (_ : below_form a0 j), below_form b j) (_ : below_form (vimp (@cons Int a l) a0) j), below_form (vimp (@cons Int a l) b) j *)
simpl in |- *; intros i l ih a b below_ab below_a.
(* Goal: below_form a j *)
apply ih with (a := Imp (Atom i) a); try assumption.
(* Goal: forall (j : Int) (_ : below_form (Imp (Atom i) a) j), below_form (Imp (Atom i) b) j *)
intros j' below_ia.
(* Goal: below_form (Imp (Atom i) c) j' *)
elim below_ia; clear below_ia; intros below_i below_a0.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
assumption.
(* Goal: below_form a j *)
apply below_ab; assumption.
Qed.


Lemma below_vimp2 :
 forall (j : Int) (l : list Int) (a b c : form),
 (forall j : Int, below_form a j -> below_form b j -> below_form c j) ->
 below_form (vimp l a) j ->
 below_form (vimp l b) j -> below_form (vimp l c) j.
(* Goal: forall (j : Int) (l : list Int) (a b c : form) (_ : forall (j0 : Int) (_ : below_form a j0) (_ : below_form b j0), below_form c j0) (_ : below_form (vimp l a) j) (_ : below_form (vimp l b) j), below_form (vimp l c) j *)
intros k l.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
elim l; clear l.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp (@nil Int) a) k) (_ : below_form (vimp (@nil Int) b) k), below_form (vimp (@nil Int) c) k *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b c : form) (_ : forall (j : Int) (_ : below_form a0 j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a0) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k) (a0 b c : form) (_ : forall (j : Int) (_ : below_form a0 j) (_ : below_form b j), below_form c j) (_ : below_form (vimp (@cons Int a l) a0) k) (_ : below_form (vimp (@cons Int a l) b) k), below_form (vimp (@cons Int a l) c) k *)
intros a b c below_abc below_a below_b.
(* Goal: below_form a j *)
apply below_abc; assumption.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 b c : form) (_ : forall (j : Int) (_ : below_form a0 j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a0) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k) (a0 b c : form) (_ : forall (j : Int) (_ : below_form a0 j) (_ : below_form b j), below_form c j) (_ : below_form (vimp (@cons Int a l) a0) k) (_ : below_form (vimp (@cons Int a l) b) k), below_form (vimp (@cons Int a l) c) k *)
simpl in |- *; intros i l ih a b c below_abc below_a below_b.
(* Goal: below_form a j *)
apply ih with (a := Imp (Atom i) a) (b := Imp (Atom i) b); try assumption.
(* Goal: forall (j : Int) (_ : below_form (Imp (Atom i) a) j) (_ : below_form (Imp (Atom i) b) j), below_form (Imp (Atom i) c) j *)
intros j' below_ia below_ib.
(* Goal: below_form (Imp (Atom i) c) j' *)
elim below_ia; clear below_ia; intros below_i below_a0.
(* Goal: below_form (Imp (Atom i) c) j' *)
elim below_ib; clear below_ib; intros below_i0 below_b0.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
assumption.
(* Goal: below_form a j *)
apply below_abc; assumption.
Qed.


Lemma below_vimp_head :
 forall (j : Int) (l : list Int) (a : form),
 below_form (vimp l a) j -> below_form a j.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
intros j l; elim l; clear l.
(* Goal: below_form a j *)
intros a below_la; assumption.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 : form) (_ : below_form (vimp l a0) j), below_form a0 j) (a0 : form) (_ : below_form (vimp (@cons Int a l) a0) j), below_form a0 j *)
intros i l ih a below_la.
(* Goal: below_form a j *)
elim (ih (Imp (Atom i) a)); clear ih.
(* Goal: below_form a j *)
intros; assumption.
(* Goal: below_form a j *)
assumption.
Qed.


Lemma below_vimp_split :
 forall (j : Int) (l : list Int) (a : form),
 (forall i : Int, In i l -> Less i j) ->
 below_form a j -> below_form (vimp l a) j.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
intros j l; elim l; clear l.
(* Goal: below_form a j *)
intros; assumption.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 : form) (_ : forall (i : Int) (_ : @In Int i l), Less i j) (_ : below_form a0 j), below_form (vimp l a0) j) (a0 : form) (_ : forall (i : Int) (_ : @In Int i (@cons Int a l)), Less i j) (_ : below_form a0 j), below_form (vimp (@cons Int a l) a0) j *)
intros i l ih a below_i below_a.
(* Goal: below_form (vimp (@cons Int i l) a) j *)
apply ih with (a := Imp (Atom i) a).
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
intros i0 in0.
(* Goal: Less i j *)
(* Goal: below_form a j *)
apply below_i.
(* Goal: below_form a j *)
right; assumption.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: Less i j *)
(* Goal: below_form a j *)
apply below_i.
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
(* Goal: below_form a j *)
assumption.
Qed.


Lemma below_vimp_tail :
 forall (j : Int) (l : list Int) (a : form),
 below_form (vimp l a) j -> forall i : Int, In i l -> Less i j.
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
intros j l; elim l; clear l.
(* Goal: forall (a : form) (_ : below_form (vimp (@nil Int) a) j) (i : Int) (_ : @In Int i (@nil Int)), Less i j *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 : form) (_ : below_form (vimp l a0) j) (i : Int) (_ : @In Int i l), Less i j) (a0 : form) (_ : below_form (vimp (@cons Int a l) a0) j) (i : Int) (_ : @In Int i (@cons Int a l)), Less i j *)
intros a below_la i0 in0; inversion_clear in0.
(* Goal: forall (a : Int) (l : list Int) (_ : forall (a0 : form) (_ : below_form (vimp l a0) j) (i : Int) (_ : @In Int i l), Less i j) (a0 : form) (_ : below_form (vimp (@cons Int a l) a0) j) (i : Int) (_ : @In Int i (@cons Int a l)), Less i j *)
simpl in |- *; intros i l ih a below_la i0 in0.
(* Goal: Less i0 j *)
inversion_clear in0.
(* Goal: Less i0 j *)
(* Goal: Less i0 j *)
 rewrite <- H; clear H i0.
(* Goal: Less i j *)
(* Goal: Less i0 j *)
elim (below_vimp_head j l (Imp (Atom i) a) below_la).
(* Goal: below_form a j *)
intros; assumption.
(* Goal: below_form a j *)
apply ih with (a := Imp (Atom i) a); assumption.
Qed.


Lemma subst_vimp_head :
 forall (j : Int) (a : form) (l : list Int) (b : form),
 (forall i : Int, In i l -> Less i j) ->
 subst_form j a (vimp l b) = vimp l (subst_form j a b).
(* Goal: forall (a b c : form) (_ : forall (j : Int) (_ : below_form a j) (_ : below_form b j), below_form c j) (_ : below_form (vimp l a) k) (_ : below_form (vimp l b) k), below_form (vimp l c) k *)
intros j a l; elim l; clear l.
(* Goal: forall (b : form) (_ : forall (i : Int) (_ : @In Int i (@nil Int)), Less i j), @eq form (subst_form j a (vimp (@nil Int) b)) (vimp (@nil Int) (subst_form j a b)) *)
(* Goal: forall (a0 : Int) (l : list Int) (_ : forall (b : form) (_ : forall (i : Int) (_ : @In Int i l), Less i j), @eq form (subst_form j a (vimp l b)) (vimp l (subst_form j a b))) (b : form) (_ : forall (i : Int) (_ : @In Int i (@cons Int a0 l)), Less i j), @eq form (subst_form j a (vimp (@cons Int a0 l) b)) (vimp (@cons Int a0 l) (subst_form j a b)) *)
intros; trivial.
(* Goal: forall (a0 : Int) (l : list Int) (_ : forall (b : form) (_ : forall (i : Int) (_ : @In Int i l), Less i j), @eq form (subst_form j a (vimp l b)) (vimp l (subst_form j a b))) (b : form) (_ : forall (i : Int) (_ : @In Int i (@cons Int a0 l)), Less i j), @eq form (subst_form j a (vimp (@cons Int a0 l) b)) (vimp (@cons Int a0 l) (subst_form j a b)) *)
intros i l ih b below_l.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: @eq form (subst_form j a (vimp l (Imp (Atom i) b))) (vimp l (Imp (Atom i) (subst_form j a b))) *)
 rewrite (ih (Imp (Atom i) b)); clear ih.
change
  (vimp l (Imp (subst_form j a (Atom i)) (subst_form j a b)) =
   vimp l (Imp (Atom i) (subst_form j a b))) in |- *.
(* Goal: @eq form (vimp l (Imp (subst_form j a (Atom i)) (subst_form j a b))) (vimp l (Imp (Atom i) (subst_form j a b))) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
 rewrite (subst_form_below j a (Atom i)).
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: @In Int i (@cons Int i l) *)
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
left; trivial.
(* Goal: forall (i : Int) (_ : @In Int i l), Less i j *)
intros i0 in0.
(* Goal: Less i0 j *)
apply below_l.
(* Goal: below_form a j *)
right; assumption.
Qed.




Lemma max_int_of_form : forall a : form, {j : Int | below_form a j}.
(* Goal: forall (_ : below_form a i) (_ : Less i j), below_form a j *)
intros a; elim a; clear a.

(* Goal: @sig Int (fun j : Int => below_list (@nil form) j) *)
(* Goal: forall (a : form) (l : list form) (_ : @sig Int (fun j : Int => below_list l j)), @sig Int (fun j : Int => below_list (@cons form a l) j) *)
exists int_null.
(* Goal: below_form Falsum int_null *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
simpl in |- *.
(* Goal: True *)
(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
trivial.

(* Goal: forall i : Int, @sig Int (fun j : Int => below_form (Atom i) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (AndF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (OrF f f0) j) *)
(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
intros i; elim (int_succ i); intros i1 less1.
(* Goal: below_form a j *)
exists i1; assumption.

(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
intros a ih_a b ih_b.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_a; intros i1 below_a.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_b; intros i2 below_b.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim (max_int i1 i2).
(* Goal: forall (j : Int) (_ : or (Less i1 j) (Equal i1 j)) (_ : or (Less i2 j) (Equal i2 j)), @sig Int (fun j0 : Int => below_list (@cons form a gamma) j0) *)
intros j le1 le2.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
exists j.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
(* Goal: below_list gamma j *)
elim le1.
(* Goal: forall _ : Less i1 j, below_form a j *)
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intro lt1.
(* Goal: below_form a j *)
apply below_form_less_below_form with i1; assumption.
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intros eq1.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i1 j); assumption.
(* Goal: below_list gamma j *)
elim le2.
(* Goal: forall _ : Less i2 j, below_list gamma j *)
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intro lt2.
(* Goal: below_form a j *)
apply below_form_less_below_form with i2; assumption.
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intros eq2.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i2 j); assumption.

(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
intros a ih_a b ih_b.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_a; intros i1 below_a.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_b; intros i2 below_b.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim (max_int i1 i2).
(* Goal: forall (j : Int) (_ : or (Less i1 j) (Equal i1 j)) (_ : or (Less i2 j) (Equal i2 j)), @sig Int (fun j0 : Int => below_list (@cons form a gamma) j0) *)
intros j le1 le2.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
exists j.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
(* Goal: below_list gamma j *)
elim le1.
(* Goal: forall _ : Less i1 j, below_form a j *)
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intro lt1.
(* Goal: below_form a j *)
apply below_form_less_below_form with i1; assumption.
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intros eq1.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i1 j); assumption.
(* Goal: below_list gamma j *)
elim le2.
(* Goal: forall _ : Less i2 j, below_list gamma j *)
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intro lt2.
(* Goal: below_form a j *)
apply below_form_less_below_form with i2; assumption.
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intros eq2.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i2 j); assumption.

(* Goal: forall (f : form) (_ : @sig Int (fun j : Int => below_form f j)) (f0 : form) (_ : @sig Int (fun j : Int => below_form f0 j)), @sig Int (fun j : Int => below_form (Imp f f0) j) *)
intros a ih_a b ih_b.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_a; intros i1 below_a.
(* Goal: @sig Int (fun j : Int => below_form (Imp a b) j) *)
elim ih_b; intros i2 below_b.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim (max_int i1 i2).
(* Goal: forall (j : Int) (_ : or (Less i1 j) (Equal i1 j)) (_ : or (Less i2 j) (Equal i2 j)), @sig Int (fun j0 : Int => below_list (@cons form a gamma) j0) *)
intros j le1 le2.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
exists j.
(* Goal: below_form (Imp a b) j *)
split.
(* Goal: below_form a j *)
(* Goal: below_list gamma j *)
elim le1.
(* Goal: forall _ : Less i1 j, below_form a j *)
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intro lt1.
(* Goal: below_form a j *)
apply below_form_less_below_form with i1; assumption.
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intros eq1.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i1 j); assumption.
(* Goal: below_list gamma j *)
elim le2.
(* Goal: forall _ : Less i2 j, below_list gamma j *)
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intro lt2.
(* Goal: below_form a j *)
apply below_form_less_below_form with i2; assumption.
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intros eq2.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i2 j); assumption.

Qed.




Lemma max_int_of_list : forall Gamma : flist, {j : Int | below_list Gamma j}.
(* Goal: forall Gamma : flist, @sig Int (fun j : Int => below_list Gamma j) *)
intros Gamma; elim Gamma; clear Gamma.
(* Goal: @sig Int (fun j : Int => below_list (@nil form) j) *)
(* Goal: forall (a : form) (l : list form) (_ : @sig Int (fun j : Int => below_list l j)), @sig Int (fun j : Int => below_list (@cons form a l) j) *)
exists int_null.
(* Goal: below_list (@nil form) int_null *)
(* Goal: forall (a : form) (l : list form) (_ : @sig Int (fun j : Int => below_list l j)), @sig Int (fun j : Int => below_list (@cons form a l) j) *)
unfold below_list in |- *; intros a in_a; inversion_clear in_a.
(* Goal: forall (a : form) (l : list form) (_ : @sig Int (fun j : Int => below_list l j)), @sig Int (fun j : Int => below_list (@cons form a l) j) *)
intros a gamma ih.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim (max_int_of_form a).
(* Goal: forall (x : Int) (_ : below_form a x), @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
intros i1 below_a.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim ih.
(* Goal: forall (x : Int) (_ : below_list gamma x), @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
intros i2 below_gamma.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
elim (max_int i1 i2).
(* Goal: forall (j : Int) (_ : or (Less i1 j) (Equal i1 j)) (_ : or (Less i2 j) (Equal i2 j)), @sig Int (fun j0 : Int => below_list (@cons form a gamma) j0) *)
intros j le1 le2.
(* Goal: @sig Int (fun j : Int => below_list (@cons form a gamma) j) *)
exists j.
(* Goal: below_list (@cons form a gamma) j *)
apply below_cons_list.
(* Goal: below_form a j *)
(* Goal: below_list gamma j *)
elim le1.
(* Goal: forall _ : Less i1 j, below_form a j *)
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intro lt1.
(* Goal: below_form a j *)
apply below_form_less_below_form with i1; assumption.
(* Goal: forall _ : Equal i1 j, below_form a j *)
(* Goal: below_list gamma j *)
intros eq1.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i1 j); assumption.
(* Goal: below_list gamma j *)
elim le2.
(* Goal: forall _ : Less i2 j, below_list gamma j *)
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intro lt2.
(* Goal: below_form a j *)
apply below_list_less_below_list with i2; assumption.
(* Goal: forall _ : Equal i2 j, below_list gamma j *)
intros eq2.
(* Goal: below_form a j *)
 rewrite <- (equal_eq i2 j); assumption.
Qed.



