(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
  Require Coq.funind.Recdef.

Local Open Scope nat_scope.

Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A)  :=
{ af_unage : forall x':A, exists x, age1 x = Some x'
; af_level1 : forall x, age1 x = None <-> level x = 0
; af_level2 : forall x y, age1 x = Some y -> level x = S (level y)
}.

Arguments af_unage [A] [level] [age1] _ _.
Arguments af_level1 [A] [level] [age1] _ _.
Arguments af_level2 [A] [level] [age1] _ _ _ _.

Class ageable (A:Type) := mkAgeable
{ level : A -> nat
; age1 : A -> option A
; age_facts : ageable_facts A level age1
}.

Definition age {A} `{ageable A} (x y:A) := age1 x = Some y.

Lemma af_wf {A} `{ageable A} :
 well_founded (fun x y => age y x).
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
  intro.
(* Goal: @Acc A (fun x y : A => @age A H y x) a *)
  remember (level a).
(* Goal: @Acc A (fun x y : A => @age A H y x) a *)
  revert a Heqn.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  induction n; intros; constructor; intros.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  apply (af_level2 age_facts) in H0.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  rewrite H0 in Heqn.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  inversion Heqn.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  copy H0.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  apply (af_level2 age_facts) in H0.
(* Goal: @Acc A (fun x y : A => @age A H y x) y *)
  apply IHn.
(* Goal: le n' m *)
  omega.
Qed.
Arguments af_wf [A] _ _.

Definition age_induction {A} `{ageable A} :=
  well_founded_induction (af_wf _).

Definition fashionR {A1} `{ageable A1} {A2}`{ageable A2} (x:A1) (y: A2) : Prop :=
  level x = level y.

Lemma fashionR_refl {A} `{ageable A} : reflexive _ fashionR.
Proof.
(* Goal: reflexive A (@fashionR A H A H) *)
  repeat intro; hnf; auto.
Qed.

Lemma fashionR_trans {A} `{ageable A} {B} `{ageable B} {C} `{ageable C} :
    forall (x: A) (y: B) (z: C), fashionR x y -> fashionR y z -> fashionR x z.
Proof.
(* Goal: forall (x : A) (y : B) (z : C) (_ : @fashionR A H B H0 x y) (_ : @fashionR B H0 C H1 y z), @fashionR A H C H1 x z *)
  unfold fashionR; intros; congruence.
Qed.

Lemma fashionR_sym {A} `{ageable A} {B} `{ageable B}:
   forall (x: A) (y: B), fashionR x y -> fashionR y x.
Proof.
(* Goal: forall (x : A) (y : B) (_ : @fashionR A H B H0 x y), @fashionR B H0 A H y x *)
  unfold fashionR; intros; auto.
Qed.

Lemma age_level {A} `{ageable A} : forall (x y:A),
  age x y -> level x = S (level y).
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: @eq nat (@level A ag (g x)) (S (@level A ag a)) *)
  apply (af_level2 age_facts); auto.
Qed.

Lemma age1_level0 {A} `{ageable A} : forall (x:A),
  age1 x = None <-> level x = 0.
Proof.
(* Goal: forall x : A, iff (@eq (option A) (@age1 A H x) (@None A)) (@eq nat (@level A H x) O) *)
  intros; apply (af_level1 age_facts).
Qed.

Section level'.
  Variable A:Type.
  Variable ag:ageable A.

  Function level' (x:A) { wf (fun x y => @age A ag y x)  x } : nat :=
(*  Function level' (x:A) { wf (transp _ (@age A ag)) x } : nat := *)
    match age1 x with
    | None => 0
    | Some x' => S (level' x')
    end.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros. hnf. assumption.
    unfold transp. apply (af_wf _).
  Defined.

  Theorem level_level' : forall x:A, level x = level' x.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intro x; induction x using age_induction; intros.
(* Goal: @ex nat (fun n : nat => @eq nat (level' A H x) (S n)) *)
    rewrite level'_equation.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    case_eq (age1 x); intros.
(* Goal: @eq nat (@level A ag x) (S (level' a)) *)
(* Goal: @eq nat (@level A ag x) O *)
    rewrite (af_level2 age_facts x a); auto.
(* Goal: @eq nat (@level B agB b) O *)
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0; auto.
  Qed.
End level'.

Lemma levelS_age1 {A} `{ageable A} : forall (x:A) n,
  level x = S n ->
  exists y, age1 x = Some y.
Proof.
(* Goal: forall (x : A) (n : nat) (_ : @eq nat (@level A H x) (S n)), @ex A (fun y : A => @eq (option A) (@age1 A H x) (@Some A y)) *)
  intros; rewrite level_level' in H0.
(* Goal: @ex A (fun y : A => @eq (option A) (@age1 A H x) (@Some A y)) *)
  rewrite level'_equation in H0.
(* Goal: @ex nat (fun n : nat => @eq nat match @age1 A H x with | Some x' => S (level' A H x') | None => O end (S n)) *)
  destruct (age1 x); eauto.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
  inv H0.
Qed.

Lemma age1_levelS {A} `{ageable A} : forall (x y:A),
  age1 x = Some y ->
  exists n, level x = S n.
Proof.
(* Goal: forall (x y : A) (_ : @eq (option A) (@age1 A H x) (@Some A y)), @ex nat (fun n : nat => @eq nat (@level A H x) (S n)) *)
  intros; rewrite level_level'.
(* Goal: @ex nat (fun n : nat => @eq nat (level' A H x) (S n)) *)
  rewrite level'_equation.
(* Goal: @ex nat (fun n : nat => @eq nat match @age1 A H x with | Some x' => S (level' A H x') | None => O end (S n)) *)
  destruct (age1 x); eauto.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
  inv H0.
Qed.

Lemma age1_level0_absurd {A} `{ageable A} : forall (x y:A),
  age1 x = Some y ->
  level x = 0 ->
  False.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: @eq (option B) (@Some B (f a)) (@None B) *)
(* Goal: @eq nat (@level A ag (g x)) O *)
  rewrite <- age1_level0 in H1.
(* Goal: @eq (option B) (@Some B (f a)) (@None B) *)
(* Goal: @eq nat (@level A ag (g x)) O *)
  rewrite H0 in H1; discriminate.
Qed.

Lemma age1None_levelS_absurd {A} `{ageable A} : forall (x:A) n,
  age1 x = None ->
  level x = S n ->
  False.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: False *)
  rewrite age1_level0 in H0.
(* Goal: @eq (option B) (@Some B (f a)) (@None B) *)
(* Goal: @eq nat (@level A ag (g x)) O *)
  rewrite H0 in H1; discriminate.
Qed.

Section RtRft.
  Variable A:Type.
  Variable R:relation A.

  Let Rt := clos_trans A R.
  Let Rft := clos_refl_trans A R.

  Lemma Rt_Rft : forall x y, Rt x y -> Rft x y.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros; elim H; intros.
(* Goal: Rft x0 y0 *)
(* Goal: Rft x0 z *)
    apply rt_step; auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    eapply rt_trans; eauto.
  Qed.

  Lemma Rt_Rft_trans : forall x y z, Rt x y -> Rft y z -> Rt x z.
  Proof.
(* Goal: forall (x y z : A) (_ : Rt x y) (_ : Rft y z), Rt x z *)
    intros x y z H H1; revert x H; elim H1; intros; auto.
(* Goal: Rt x0 z *)
    eapply t_trans; eauto; apply t_step; auto.
  Qed.

  Lemma Rft_Rt_trans : forall x y z, Rft x y -> Rt y z -> Rt x z.
  Proof.
(* Goal: forall (x y z : A) (_ : Rft x y) (_ : Rt y z), Rt x z *)
    intros x y z H; revert z; elim H; intros; auto.
(* Goal: Rt x0 z *)
    eapply t_trans; eauto; apply t_step; auto.
  Qed.

  Lemma transpose_clos_trans : forall A R x y,
    clos_trans A (transp A R) x y <-> transp A (clos_trans A R) x y.
  Proof.
(* Goal: forall (A : Type) (R : relation A) (x y : A), iff (clos_trans A (transp A R) x y) (transp A (clos_trans A R) x y) *)
    unfold transp; intuition.

(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    elim H; intros.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) y0 x0 *)
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
    apply t_step; auto.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
    apply t_trans with y0; auto.

(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    elim H; intros.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) y0 x0 *)
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
    apply t_step; auto.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
    apply t_trans with y0; auto.
  Qed.
End RtRft.

Hint Resolve rt_refl.

Definition laterR {A} `{ageable A} : relation A := clos_trans A age.
Definition necR   {A} `{ageable A} : relation A := clos_refl_trans A age.

Require Coq.Wellfounded.Wellfounded.
Lemma laterR_wf {A} `{ageable A} :
  well_founded (transp _ laterR).
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
  hnf; intro.
  induction a using
    (well_founded_induction (Wellfounded.Transitive_Closure.wf_clos_trans _ (fun x y => age y x) (af_wf _))).
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  constructor; intros.
(* Goal: @Acc A (transp A (@laterR A H)) y *)
  unfold laterR in H1.
(* Goal: @Acc A (transp A (@laterR A H)) y *)
  rewrite <- transpose_clos_trans in H1.
(* Goal: @Acc A (transp A (@laterR A H)) y *)
  apply H0; auto.
Qed.

Definition laterR_induction {A} `{ageable A} :=
  @well_founded_induction A (transp A laterR) laterR_wf.

Lemma age_irreflexive {A}  `{ageable A}: forall x, age x x -> False.
Proof.
(* Goal: forall (x : A) (_ : @laterR A HA x x), False *)
  intros x.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  induction x using age_induction; intros.
(* Goal: False *)
  apply H0 with x; auto.
Qed.

Lemma laterR_irreflexive {A} `{HA: ageable A} : forall x, laterR x x -> False.
Proof.
(* Goal: forall (x : A) (_ : @laterR A HA x x), False *)
  intros x.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  induction x using laterR_induction; intros.
(* Goal: False *)
  apply H with x; auto.
Qed.

Lemma nec_refl_or_later {A} `{ageable A} : forall x y,
  necR x y -> x = y \/ laterR x y.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: or (@eq A x y) (@laterR A H x y) *)
  elim H0; intros; auto.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) y0 x0 *)
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
  right; apply t_step; auto.
(* Goal: or (@eq A x0 z) (@laterR A H x0 z) *)
  destruct H2; destruct H4; subst; auto.
(* Goal: clos_trans A0 (fun x y : A0 => R0 y x) z x0 *)
  right; apply t_trans with y0; auto.
Qed.

Lemma necR_antisym {A} `{ageable A} : forall x y,
  necR x y -> necR y x -> x = y.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: @eq A x y *)
  apply nec_refl_or_later in H0.
(* Goal: @eq A x y *)
  apply nec_refl_or_later in H1.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
  intuition.
(* Goal: @eq A x y *)
  elim (laterR_irreflexive x).
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
  eapply t_trans; eauto.
Qed.

Lemma age_later_nec {A} `{HA: ageable A} : forall x y z,
  age x y ->
  laterR x z ->
  necR y z.
Proof.
(* Goal: forall (x y z : A) (_ : @age A HA x y) (_ : @laterR A HA x z), @necR A HA y z *)
  intros x y z H H1; revert y H.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  induction H1; intros.
(* Goal: @necR A HA y0 y *)
(* Goal: @necR A HA y0 z *)
  replace y0 with y.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
  apply rt_refl.
(* Goal: @eq A y y0 *)
(* Goal: @necR A HA y0 z *)
  unfold age in *; congruence.
(* Goal: clos_refl_trans A (@age A agA) x z *)
  apply rt_trans with y; auto.
(* Goal: clos_refl_trans A (@age A HA) y0 y *)
(* Goal: clos_refl_trans A (@age A HA) y z *)
  apply IHclos_trans1; auto.
(* Goal: clos_refl_trans A (@age A HA) y z *)
  apply Rt_Rft; auto.
Qed.

Lemma necR_level {A} `{X: ageable A} : forall (x y:A),
  necR x y ->
  level x >= level y.
Proof.
(* Goal: forall (x y : A) (_ : @laterR A X x y), gt (@level A X x) (@level A X y) *)
  intros x y H; induction H; auto.
(* Goal: gt (@level A X x) (@level A X y) *)
(* Goal: gt (@level A X x) (@level A X z) *)
  rewrite (age_level x y); auto.
(* Goal: le n' m *)
  omega.
Qed.

Lemma laterR_level {A} `{X: ageable A} : forall (x y:A),
  laterR x y ->
  level x > level y.
Proof.
(* Goal: forall (x y : A) (_ : @laterR A X x y), gt (@level A X x) (@level A X y) *)
  intros x y H; induction H; auto.
(* Goal: gt (@level A X x) (@level A X y) *)
(* Goal: gt (@level A X x) (@level A X z) *)
  rewrite (age_level x y); auto.
(* Goal: le n' m *)
  omega.
Qed.

Section NAT_AGEABLE.

  Definition natLevel (x:nat) : nat := x.
  Definition natAge1 (x:nat) : option nat :=
    match x with
    | 0 => None
    | S n => Some n
    end.
  Definition natUnage (x:nat) : nat := S x.

  Lemma ag_nat_facts :
    ageable_facts nat natLevel natAge1.
  Proof.
(* Goal: ageable_facts (prod A B) levelAB age1AB *)
    constructor.
(* Goal: forall x' : nat, @ex nat (fun x : nat => @eq (option nat) (natAge1 x) (@Some nat x')) *)
(* Goal: forall x : nat, iff (@eq (option nat) (natAge1 x) (@None nat)) (@eq nat (natLevel x) O) *)
(* Goal: forall (x y : nat) (_ : @eq (option nat) (natAge1 x) (@Some nat y)), @eq nat (natLevel x) (S (natLevel y)) *)
    intros; exists (S x'); compute; auto.
(* Goal: forall x : nat, iff (@eq (option nat) (natAge1 x) (@None nat)) (@eq nat (natLevel x) O) *)
(* Goal: forall (x y : nat) (_ : @eq (option nat) (natAge1 x) (@Some nat y)), @eq nat (natLevel x) (S (natLevel y)) *)
    intro x; destruct x; intuition; inv H.
    firstorder;
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
      destruct x; inv H; compute; eauto.
  Qed.

  Definition ag_nat : ageable nat :=
    mkAgeable nat natLevel natAge1 ag_nat_facts.

  Lemma nec_nat : forall (n n':nat),
    @necR _ ag_nat n n' <-> n' <= n.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros. split; intro.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: le y x *)
(* Goal: le x x *)
(* Goal: le z x *)
(* Goal: @necR nat ag_nat n n' *)
    destruct x; inv H; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    auto.
(* Goal: le n' m *)
    omega.

(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_refl.
(* Goal: @necR nat ag_nat (S m) n' *)
    apply rt_trans with m.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply rt_step. compute; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    auto.
  Qed.

  Lemma later_nat : forall (n n':nat),
    @laterR _ ag_nat n n' <-> n' < n.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros. split; intro.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: lt y x *)
(* Goal: lt z x *)
(* Goal: @laterR nat ag_nat n n' *)
    destruct x; simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    inv H.
(* Goal: le n' m *)
    inv H. omega.
(* Goal: le n' m *)
    omega.
(* Goal: @eq (option (prod A B)) (@age1 (prod A B) ag_prod' (@pair A B x' x)) (@Some (prod A B) (@pair A B x' y)) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    hnf in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    inv H.
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' y) *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply t_step.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    compute; auto.
(* Goal: @laterR nat ag_nat (S m) n' *)
    apply Rt_Rft_trans with m.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply t_step. compute; auto.
(* Goal: clos_refl_trans nat (@age nat ag_nat) m n' *)
    change (@necR _ ag_nat m n').
(* Goal: @necR nat ag_nat m n' *)
    rewrite nec_nat.
(* Goal: le n' m *)
    omega.
  Qed.

End NAT_AGEABLE.


Lemma laterR_level' {A} `{H : ageable A}: forall {w1 w2: A}, laterR w1 w2 -> @laterR _ ag_nat (level w1) (level w2).
Proof.
(* Goal: forall (w1 w2 : A) (_ : @laterR A H w1 w2), @laterR nat ag_nat (@level A H w1) (@level A H w2) *)
induction 1.
(* Goal: clos_refl_trans nat (@age nat ag_nat) (S m) m *)
(* Goal: clos_refl_trans nat (@age nat ag_nat) m (@level A H y) *)
constructor 1. apply age_level in H0. rewrite H0; reflexivity.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
constructor 2 with (level y); auto.
Qed.

Lemma necR_nat {A} `{H : ageable A}:
    forall {x y: A}, necR x y -> @necR nat ag_nat (level x) (level y).
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros. apply necR_level in H0.
(* Goal: @necR nat ag_nat (@level A H x) (@level A H y) *)
     induction H0; simpl in *. constructor 2.
(* Goal: ageable_facts (prod A B) levelAB age1AB *)
     constructor 3 with m. constructor 1. constructor.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
     auto.
  Qed.

Section BIJECTION.
  Variable A B : Type.
  Variable ag: ageable A.
  Variable bijAB: bijection A B.

  Let levelB (x:B) : nat :=
    level (bij_g _ _ bijAB x).

  Let age1B  (x: B) : option B :=
     match age1 (bij_g _ _ bijAB x) with
     | Some y => Some (bij_f _ _ bijAB y)
     | None => None
     end.

  Let ageB (x y: B) :=age1B x = Some y.

  Lemma age_bij_unage :
    forall x', exists x, age1B x = Some x'.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    unfold age1B, levelB; simpl; intros.
(* Goal: @eq nat (@level A ag (bij_g A B bijAB x)) (S (@level A ag (bij_g A B bijAB y))) *)
    destruct bijAB as [f g fg gf]; simpl in *.
(* Goal: @ex B (fun x : B => @eq (option B) match @age1 A ag (g x) with | Some y => @Some B (f y) | None => @None B end (@Some B x')) *)
    destruct (af_unage age_facts (g x')) as [y ?].
(* Goal: @ex B (fun x : B => @eq (option B) match @age1 A ag (g x) with | Some y => @Some B (f y) | None => @None B end (@Some B x')) *)
   exists (f y). rewrite gf. rewrite H. f_equal. apply fg.
  Qed.

  Lemma age_bij_level1 :
    forall x, age1B x = None <-> levelB x = 0.
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros.
(* Goal: iff (@eq (option B) (age1B x) (@None B)) (@eq nat (levelB x) O) *)
    unfold age1B, levelB; simpl.
(* Goal: iff (@eq (option B) match @age1 A ag (bij_g A B bijAB x) with | Some y => @Some B (bij_f A B bijAB y) | None => @None B end (@None B)) (@eq nat (@level A ag (bij_g A B bijAB x)) O) *)
    destruct bijAB as [f g fg gf]; simpl.
(* Goal: iff (@eq (option B) match @age1 A ag (g x) with | Some y => @Some B (f y) | None => @None B end (@None B)) (@eq nat (@level A ag (g x)) O) *)
    case_eq (age1 (g x)); intuition; try discriminate.
(* Goal: @eq (option B) (@Some B (f a)) (@None B) *)
(* Goal: @eq nat (@level A ag (g x)) O *)
    rewrite <- age1_level0 in H1.
(* Goal: @eq (option B) (@Some B (f a)) (@None B) *)
(* Goal: @eq nat (@level A ag (g x)) O *)
    rewrite H0 in H1; discriminate.
(* Goal: @eq nat (@level B agB b) O *)
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0; auto.
  Qed.

  Lemma age_bij_level2 :
    forall x y, age1B x = Some y -> levelB x = S (levelB y).
  Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros.
(* Goal: @eq nat (levelB x) (S (levelB y)) *)
    unfold age1B, levelB in *; simpl in *.
(* Goal: @eq nat (@level A ag (bij_g A B bijAB x)) (S (@level A ag (bij_g A B bijAB y))) *)
    destruct bijAB as [f g fg gf]; simpl in *.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 (g x)); intros; rewrite H0 in H; inv H.
(* Goal: @eq nat (@level A ag (g x)) (S (@level A ag (g (f a)))) *)
    rewrite gf.
(* Goal: @eq nat (@level A ag (g x)) (S (@level A ag a)) *)
    apply (af_level2 age_facts); auto.
  Qed.

  Lemma ag_bij_facts : ageable_facts B levelB age1B.
  Proof.
(* Goal: ageable_facts (prod A B) levelAB age1AB *)
    constructor.
(* Goal: forall x' : B, @ex B (fun x : B => @eq (option B) (age1B x) (@Some B x')) *)
(* Goal: forall x : B, iff (@eq (option B) (age1B x) (@None B)) (@eq nat (levelB x) O) *)
(* Goal: forall (x y : B) (_ : @eq (option B) (age1B x) (@Some B y)), @eq nat (levelB x) (S (levelB y)) *)
    exact age_bij_unage.
(* Goal: forall x : B, iff (@eq (option B) (age1B x) (@None B)) (@eq nat (levelB x) O) *)
(* Goal: forall (x y : B) (_ : @eq (option B) (age1B x) (@Some B y)), @eq nat (levelB x) (S (levelB y)) *)
    exact age_bij_level1.
(* Goal: forall (x y : B) (_ : @eq (option B) (age1B x) (@Some B y)), @eq nat (levelB x) (S (levelB y)) *)
    exact age_bij_level2.
  Qed.

  Definition ag_bij : ageable B :=
    mkAgeable B levelB age1B ag_bij_facts.
End BIJECTION.

Section PROD.
  Variable A B : Type.
  Variable agA: ageable A.

  Let levelAB (x:prod A B) := level (fst x).
  Let age1AB (x:prod A B) :=
    match age1 (fst x) with
    | None => None
    | Some a' => Some (a',snd x)
    end.

  Lemma ag_prod_facts : ageable_facts (prod A B) levelAB age1AB.
  Proof.
(* Goal: ageable_facts (prod A B) levelAB age1AB *)
    constructor.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    unfold levelAB, age1AB; simpl; intros.
(* Goal: @ex (prod A B) (fun x : prod A B => @eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) *)
(* Goal: forall x : prod A B, iff (@eq (option (prod A B)) (age1AB x) (@None (prod A B))) (@eq nat (levelAB x) O) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    destruct (af_unage age_facts (fst x')) as [y1 ?].
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    exists (y1, snd x'). simpl. rewrite H. f_equal. destruct x'; auto.
(* Goal: forall x : prod A B, iff (@eq (option (prod A B)) (age1AB x) (@None (prod A B))) (@eq nat (levelAB x) O) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    intros [a b]; firstorder.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H; simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 a); intros; rewrite H0 in H; inv H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    unfold levelAB; simpl.
(* Goal: @eq nat (@level B agB b) O *)
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0; auto.
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    unfold levelAB in H.
(* Goal: @necR A agA w w' *)
    simpl in H.
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0 in H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    unfold age1AB; simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    rewrite H; auto.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H.
(* Goal: @eq nat (levelAB x) (S (levelAB y)) *)
    unfold levelAB.
(* Goal: @eq nat (@level B agB (@snd A B x)) (S (@level B agB (@snd A B y))) *)
    destruct x; simpl in *.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 a); intros; rewrite H0 in H; inv H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply age_level; auto.
  Qed.

  Definition ag_prod :=
    mkAgeable (prod A B) levelAB age1AB ag_prod_facts.

  Lemma prod_nec_split : forall n x n' x',
    @necR (prod A B) ag_prod (n,x) (n',x') <-> necR n n' /\ x = x'.
  Proof.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    intros; split; intro.
(* Goal: and (@laterR A agA n n') (@eq B x x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    remember (n,x) as w.
(* Goal: and (@laterR A agA n n') (@eq B x x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    remember (n',x') as w'.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    revert n x n' x' Heqw Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    induction H; simpl; intros; subst; auto.
(* Goal: @necR A agA w w' *)
    unfold age in H. simpl in H.
(* Goal: @necR A agA w w' *)
    unfold age1AB in H. simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 n); intros; rewrite H0 in H; inv H.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply rt_step. auto.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    inv Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_refl.
(* Goal: and (@necR A agA n n') (@eq B x0 x') *)
(* Goal: @necR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    specialize (IHclos_refl_trans1 n x0 (fst y) (snd y)).
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans1; destruct y; auto.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
    simpl in *.
(* Goal: and (@necR A agA n n') (@eq B x0 x') *)
(* Goal: @necR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    specialize (IHclos_refl_trans2 a b n' x').
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans2; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans2; auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    intuition. eapply rt_trans; eauto.
(* Goal: @eq A x0 x' *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    congruence.

(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    destruct H; subst.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: @age (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' y) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_step. hnf.
(* Goal: @eq (option (prod A B)) (@age1 (prod A B) ag_prod' (@pair A B x' x)) (@Some (prod A B) (@pair A B x' y)) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    hnf in H. simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    unfold age1AB. simpl. rewrite H. auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_refl.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    eapply rt_trans; eauto.
  Qed.

  Lemma prod_later_split : forall n x n' x',
    @laterR (prod A B) ag_prod (n,x) (n',x') <-> laterR n n' /\ x = x'.
  Proof.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    intros; split; intro.
(* Goal: and (@laterR A agA n n') (@eq B x x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    remember (n,x) as w.
(* Goal: and (@laterR A agA n n') (@eq B x x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    remember (n',x') as w'.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    revert n x n' x' Heqw Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    induction H; simpl; intros; subst; auto.
(* Goal: @necR A agA w w' *)
    unfold age in H. simpl in H.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H; simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 n); intros; rewrite H0 in H; inv H.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply t_step. compute. auto.
(* Goal: and (@laterR A agA n n') (@eq B x0 x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    specialize (IHclos_trans1 n x0 (fst y) (snd y)).
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans1; destruct y; auto.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
    simpl in *.
(* Goal: and (@laterR A agA n n') (@eq B x0 x') *)
(* Goal: @laterR (prod A B) ag_prod (@pair A B n x) (@pair A B n' x') *)
    specialize (IHclos_trans2 a b n' x').
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans2; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans2; auto.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    intuition. eapply t_trans; eauto.
(* Goal: @eq A x0 x' *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    congruence.

(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    destruct H; subst.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' y) *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply t_step.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    hnf; simpl. unfold age1AB. simpl; rewrite H. auto.
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    eapply t_trans; eauto.
  Qed.

End PROD.

Section PROD'.
  Variable A B : Type.
  Variable agB: ageable B.

  Let levelAB (x:prod A B) := level (snd x).
  Let age1AB (x:prod A B) :=
    match age1 (snd x) with
    | None => None
    | Some a' => Some (fst x, a')
    end.

  Lemma ag_prod'_facts : ageable_facts (prod A B) levelAB age1AB.
  Proof.
(* Goal: ageable_facts (prod A B) levelAB age1AB *)
    constructor.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    unfold levelAB, age1AB; simpl; intros.
(* Goal: @ex (prod A B) (fun x : prod A B => @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) *)
(* Goal: forall x : prod A B, iff (@eq (option (prod A B)) (age1AB x) (@None (prod A B))) (@eq nat (levelAB x) O) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    destruct (af_unage age_facts (snd x')) as [y2 ?].
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    exists (fst x', y2). simpl. rewrite H. f_equal. destruct x'; auto.
(* Goal: forall x : prod A B, iff (@eq (option (prod A B)) (age1AB x) (@None (prod A B))) (@eq nat (levelAB x) O) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    intros [a b]; firstorder.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H; simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 b); intros; rewrite H0 in H; inv H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    unfold levelAB; simpl.
(* Goal: @eq nat (@level B agB b) O *)
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0; auto.
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    unfold levelAB in H.
(* Goal: @necR A agA w w' *)
    simpl in H.
(* Goal: @eq (option (prod A B)) (age1AB (@pair A B a b)) (@None (prod A B)) *)
(* Goal: forall (x y : prod A B) (_ : @eq (option (prod A B)) (age1AB x) (@Some (prod A B) y)), @eq nat (levelAB x) (S (levelAB y)) *)
    rewrite <- age1_level0 in H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    unfold age1AB; simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    rewrite H; auto.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
    intros.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H.
(* Goal: @eq nat (levelAB x) (S (levelAB y)) *)
    unfold levelAB.
(* Goal: @eq nat (@level B agB (@snd A B x)) (S (@level B agB (@snd A B y))) *)
    destruct x; simpl in *.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 b); intros; rewrite H0 in H; inv H.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
    simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply age_level; auto.
  Qed.

  Definition ag_prod' :=
    mkAgeable (prod A B) levelAB age1AB ag_prod'_facts.

  Lemma prod'_nec_split : forall n x n' x',
    @necR (prod A B) ag_prod' (x,n) (x',n') <-> necR n n' /\ x = x'.
  Proof.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    intros; split; intro.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    remember (x,n) as w.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    remember (x',n') as w'.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    revert n x n' x' Heqw Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    induction H; simpl; intros; subst; auto.
(* Goal: @necR A agA w w' *)
    unfold age in H. simpl in H.
(* Goal: @necR A agA w w' *)
    unfold age1AB in H. simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 n); intros; rewrite H0 in H; inv H.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply rt_step. auto.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    inv Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_refl.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    specialize (IHclos_refl_trans1 n x0 (snd y) (fst y)).
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans1; destruct y; auto.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
    simpl in *.
(* Goal: and (@necR B agB n n') (@eq A x0 x') *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    specialize ( IHclos_refl_trans2 b a n' x').
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans2; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_refl_trans2; auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    intuition. eapply rt_trans; eauto.
(* Goal: @eq A x0 x' *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    congruence.

(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    destruct H; subst.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: @age (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' y) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_step. hnf.
(* Goal: @eq (option (prod A B)) (@age1 (prod A B) ag_prod' (@pair A B x' x)) (@Some (prod A B) (@pair A B x' y)) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    hnf in H. simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    unfold age1AB. simpl. rewrite H. auto.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' x) *)
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply rt_refl.
(* Goal: @necR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    eapply rt_trans; eauto.
  Qed.

  Lemma prod'_later_split : forall n x n' x',
    @laterR (prod A B) ag_prod' (x,n) (x',n') <-> laterR n n' /\ x = x'.
  Proof.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    intros; split; intro.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    remember (x,n) as w.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    remember (x',n') as w'.
(* Goal: and (@laterR B agB n n') (@eq A x x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    revert n x n' x' Heqw Heqw'.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    induction H; simpl; intros; subst; auto.
(* Goal: @necR A agA w w' *)
    unfold age in H. simpl in H.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    unfold age1AB in H; simpl in H.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
    case_eq (age1 n); intros; rewrite H0 in H; inv H.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    split; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    apply t_step. compute. auto.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    specialize (IHclos_trans1 n x0 (snd y) (fst y)).
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans1; destruct y; auto.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
    simpl in *.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    specialize ( IHclos_trans2 b a n' x').
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans2; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    spec IHclos_trans2; auto.
(* Goal: and (@laterR B agB n n') (@eq A x0 x') *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    intuition. eapply t_trans; eauto.
(* Goal: @eq A x0 x' *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    congruence.

(* Goal: @laterR (prod A B) ag_prod' (@pair A B x n) (@pair A B x' n') *)
    destruct H; subst.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
    induction H.
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' y) *)
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    apply t_step.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
    hnf; simpl. unfold age1AB. simpl; rewrite H. auto.
(* Goal: @laterR (prod A B) ag_prod' (@pair A B x' x) (@pair A B x' z) *)
    eapply t_trans; eauto.
  Qed.

End PROD'.

Fixpoint composeOptN (A: Type) (f: A -> option A)
         (n: nat) (w: A) {struct n} : option A :=
 match n  with
 | S n' => match f w with Some w' => composeOptN A f n' w' | None => None end
 | O => Some w
 end.
Arguments composeOptN [A] _ _ _.

Definition ageN {A} `{ageable A}: nat -> A -> option A := composeOptN age1.

Lemma ageN1  {A} `{ageable A}: ageN 1 = age1.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
unfold ageN. simpl.
(* Goal: @eq (forall _ : A, option A) (fun w : A => match @age1 A H w with | Some w' => @Some A w' | None => @None A end) (@age1 A H) *)
extensionality phi.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
case_eq (age1 phi); intros; try rewrite H; auto.
Qed.

Lemma ageN_compose {A} `{agA : ageable A}:
 forall a b c phi1 phi2 phi3,ageN a phi1 = Some phi2 ->
       ageN b phi2 = Some phi3 ->  (a+b=c)%nat ->  ageN c phi1 = Some phi3.
Proof.
(* Goal: False *)
unfold ageN in *.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
induction a; simpl; intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
subst. inversion H; clear H. auto.
(* Goal: @eq (option A) (@composeOptN A (@age1 A agA) c phi1) (@Some A phi3) *)
subst c.
(* Goal: @eq (option A) (@composeOptN A (@age1 A agA) (S (Init.Nat.add a b)) phi1) (@Some A phi3) *)
case_eq (age1 phi1); intros; rewrite H1 in H; try discriminate.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
simpl.
(* Goal: @eq (option A) match @age1 A H phi with | Some w' => @Some A w' | None => @None A end (@None A) *)
rewrite H1.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eapply IHa; eauto.
Qed.

Lemma ageN_compose' {A} `{agA : ageable A}:
  forall a b phi1 phi3,
   ageN (a+b)%nat phi1 = Some phi3 -> exists phi2, ageN a phi1 = Some phi2 /\ ageN b phi2 = Some phi3.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
case_eq (ageN a phi1); intros.
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@Some A a0) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
rename a0 into phi.
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@Some A phi) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
exists phi.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
split; auto.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
case_eq (ageN b phi); intros.
(* Goal: @eq (option A) (@Some A a0) (@Some A phi3) *)
(* Goal: @eq (option A) (@None A) (@Some A phi3) *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
rename a0 into phi0.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
generalize (ageN_compose a b (a+b) phi1 _ _ H0 H1 (refl_equal _)); intro.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
rewrite H in H2; auto.
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
elimtype False.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert phi1 phi H H1 H0; induction a; intros.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
simpl in *.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
inv H0.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
rewrite H in H1; discriminate.
(* Goal: le n' m *)
replace (S a + b)%nat with (S (a+b))%nat in H by omega.
unfold ageN in *;
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
simpl in *.
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
case_eq (age1 phi1); intros; rewrite H2 in H; try discriminate.
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
rewrite H2 in H0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eapply IHa; eauto.
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
elimtype False.
(* Goal: False *)
unfold ageN in *.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert phi1 H H0; induction a; intros.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
simpl in *. discriminate.
(* Goal: le n' m *)
replace (S a + b)%nat with (S (a+b))%nat in H by omega.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
simpl in *.
(* Goal: False *)
(* Goal: False *)
revert H H0; case_eq (age1 phi1); intros; try discriminate.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eapply IHa; eauto.
Qed.

Lemma necR_evolve {A} `{agA : ageable A}:
    necR = fun (phi phi': A) => exists n, ageN n phi = Some phi'.
Proof.
(* Goal: @eq (relation A) (@necR A agA) (fun phi phi' : A => @ex nat (fun n : nat => @eq (option A) (@ageN A agA n phi) (@Some A phi'))) *)
extensionality w w'.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
apply prop_ext; split; intros.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
unfold necR in H.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n w) (@Some A w')) *)
(* Goal: @necR A agA w w' *)
induction H.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A y)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
exists 1%nat. rewrite ageN1.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
exists O; auto.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
destruct IHclos_refl_trans1 as [n1 ?].
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
destruct IHclos_refl_trans2 as [n2 ?].
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
exists (n1+n2)%nat.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eapply ageN_compose; eauto.
(* Goal: @necR A agA w w' *)
destruct H as [n ?].
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert w w' H; induction n; intros.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
inv H.
(* Goal: @necR A agA w' w' *)
(* Goal: @necR A agA w w' *)
constructor 2.
(* Goal: @necR A agA w w' *)
unfold ageN in H.
(* Goal: @necR A agA w w' *)
simpl in H.
(* Goal: False *)
(* Goal: False *)
revert H; case_eq (age1 w); intros; try discriminate.
(* Goal: @necR A agA w w' *)
constructor 3 with a.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
constructor 1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
apply IHn; auto.
Qed.

Lemma age_noetherian  {A} `{ageable A}: forall phi, exists n, ageN n phi = None.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  intros.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
  induction phi using age_induction.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n x) (@None A)) *)
  rename x into phi.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  case_eq (age1 phi); intros.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
  generalize H1; intros.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
  apply H0 in H1.
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
  destruct H1 as [n ?].
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A H n phi) (@None A)) *)
  exists (S n).
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
  unfold ageN; simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
  rewrite H2; auto.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
  exists (S O); simpl.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
  unfold ageN; simpl.
(* Goal: @eq (option A) match @age1 A H phi with | Some w' => @Some A w' | None => @None A end (@None A) *)
  rewrite H1.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
  auto.
Qed.

Lemma predicate_max:
  forall (F: nat -> Prop) (Fdec: forall n, {F n}+{~ F n}) n,
  F 0%nat ->
  ~ F n ->
  exists i, F i /\ (i<n)%nat /\ ~ F (S i).
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
assert (forall m, (m <= n)%nat ->
         (forall k, (k<m)%nat -> F k) \/
         (exists i, F i /\ (i<m)%nat /\ ~ F (S i))).
(* Goal: forall (m : nat) (_ : le m n), or (forall (k : nat) (_ : lt k m), F k) (@ex nat (fun i : nat => and (F i) (and (lt i m) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
induction m.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
left; intros.
(* Goal: le n' m *)
elimtype False; omega.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
intro.
(* Goal: le n' m *)
assert (m<=n)%nat; try omega.
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct (IHm H2).
(* Goal: le n' m *)
assert (m < n \/ m = n)%nat; try omega.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H4.
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct (Fdec m) as [?H|?H].
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
left.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: le n' m *)
assert (k < m \/ k = m)%nat; try omega.
(* Goal: F k *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H7.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
subst k; auto.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
(* Goal: or (@necR A H z c) (@necR A H c z) *)
right.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
exists (Peano.pred m).
(* Goal: and (F (Init.Nat.pred m)) (and (lt (Init.Nat.pred m) (S m)) (not (F (S (Init.Nat.pred m))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct m.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S O)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S (S n))) (not (F (S i))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
contradiction.
(* Goal: le n' m *)
replace (Peano.pred (S m)) with m; try omega.
(* Goal: and (F m) (and (lt m (S (S m))) (not (F (S m)))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
split.
(* Goal: le n' m *)
apply H3; try omega.
(* Goal: le n' m *)
split; try omega.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
subst m.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
(* Goal: or (@necR A H z c) (@necR A H c z) *)
right.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S n)) (not (F (S i))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct n.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S O)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S (S n))) (not (F (S i))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
contradiction.
(* Goal: le n' m *)
exists n; repeat split; auto; try omega.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
(* Goal: or (@necR A H z c) (@necR A H c z) *)
right.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H3 as [i H4].
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H4.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H4.
(* Goal: le n' m *)
exists i; repeat split; auto; omega.
(* Goal: le n' m *)
assert (n <= n)%nat; try omega.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct (H1 _ H2).
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S O)) (not (F (S i))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i (S (S n))) (not (F (S i))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct n; try contradiction.
(* Goal: le n' m *)
exists n; repeat split; auto; try omega.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
Qed.

Lemma age_noetherian'  {A} `{agA : ageable A}:
       forall phi, exists! n, exists phi', ageN n phi = Some phi' /\ age1 phi' = None.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
destruct (age_noetherian phi) as [n ?].
assert (Fdec: forall n, {ageN n phi <> None}+{~( ageN n phi <> None)})
  by (intros; destruct (ageN n0 phi); auto; left; intro Hx; inversion Hx).
destruct (predicate_max (fun n => ageN n phi <> None) Fdec n) as [i [? [? ?]]].
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
intro. inv H0.
(* Goal: forall _ : le (S m) n, or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
intro.
rewrite H in H0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
contradiction H0; auto.
exists i.
(* Goal: and (F m) (and (lt m (S (S m))) (not (F (S m)))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: or (forall (k : nat) (_ : lt k (S m)), F k) (@ex nat (fun i : nat => and (F i) (and (lt i (S m)) (not (F (S i)))))) *)
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
split.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert H0; case_eq (ageN i phi); intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
exists a; split; auto.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert H2; case_eq (ageN (S i) phi); intros.
contradiction H4.
intro Hx; inv Hx.
clear - H0 H2.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert phi a H0 H2; induction i; intros.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
inv H0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
rewrite ageN1 in H2; auto.
(* Goal: False *)
unfold ageN in *.
simpl in H0.
(* Goal: False *)
(* Goal: False *)
revert H0; case_eq (age1 phi); intros; try discriminate.
simpl in H2.
rewrite H in H2.
eapply IHi.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eauto.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
simpl.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
contradiction H3; auto.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
destruct H3 as [phi' [? ?]].
assert (ageN (S i) phi = None).
clear - H2.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert H2; case_eq (ageN (S i) phi); intros.
contradict H2. intro Hx; inv Hx.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto. clear H2.
clear - H0 H5 H3 H4.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert H0; case_eq (ageN i phi); intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
2: contradiction H0; auto.
clear H0.
assert (age1 a = None).
clear - H H5.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert phi H5 H; induction i; intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
inv H; rewrite ageN1 in H5; auto.
(* Goal: False *)
unfold ageN in *.
(* Goal: @eq (option A) (@age1 A agA x) (@Some A y) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A x)) *)
(* Goal: @ex nat (fun n : nat => @eq (option A) (@ageN A agA n x) (@Some A z)) *)
(* Goal: @necR A agA w w' *)
revert H H5; simpl. case_eq (age1 phi); intros; try discriminate.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eapply IHi; eauto.
clear H5.
assert (forall i d phi a a', ageN i phi = Some a -> ageN (i+d) phi = Some a' -> age1 a' = None -> age1 a = None -> d=0%nat).
clear.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
induction i; intros.
(* Goal: @necR A agA w w' *)
(* Goal: @necR A agA w w' *)
inv H.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct d; auto.
simpl in H0.
unfold ageN in H0. simpl in H0.
(* Goal: False *)
(* Goal: False *)
(* Goal: @ex A (fun phi2 : A => and (@eq (option A) (@None A) (@Some A phi2)) (@eq (option A) (@ageN A agA b phi2) (@Some A phi3))) *)
rewrite H2 in H0. inv H0.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
unfold ageN in H, H0. simpl in *.
(* Goal: False *)
(* Goal: False *)
revert H; case_eq (age1 phi); intros; try discriminate.
rewrite H in H0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
eauto.
(* Goal: le n' m *)
assert (i<x' \/ i=x' \/ i>x')%nat by omega.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H2 as [?| [?| ?]]; auto.
(* Goal: le n' m *)
replace x' with (i+(x'-i))%nat in H3 by omega.
specialize (H1 _ _ _ _ _ H H3 H4 H0).
(* Goal: le n' m *)
omega.
(* Goal: le n' m *)
replace i with (x'+(i-x'))%nat in H by omega.
specialize (H1 _ _ _ _ _ H3 H H0 H4).
(* Goal: le n' m *)
omega.
Qed.

Lemma ageable_ext:
   forall A (B C: ageable A),
      @age1 _ B = @age1 _ C -> @level _ B = @level _ C -> B=C.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: @eq (ageable A) B C *)
destruct B; destruct C.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
simpl in *.
(* Goal: @eq (ageable A) (mkAgeable A level0 age2 age_facts0) (mkAgeable A level1 age3 age_facts1) *)
subst age3. subst level0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
replace age_facts1 with age_facts0; auto.
(* Goal: @eq (ageable_facts A level1 age2) age_facts0 age_facts1 *)
apply proof_irr.
Qed.

Lemma necR_linear {A} `{H : ageable A}:
  forall {a b c}, necR a b -> necR a c -> necR b c \/ necR c b.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: or (@necR A H b c) (@necR A H c b) *)
apply trans_rt1n in H0.
(* Goal: or (@necR A H b c) (@necR A H c b) *)
apply trans_rt1n in H1.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
revert c H1; induction H0; intros; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
left; apply rt1n_trans; auto.
(* Goal: @eq (option A) (@composeOptN A (@age1 A agA) c phi1) (@Some A phi3) *)
(* Goal: @eq (option A) (@composeOptN A (@age1 A agA) c phi1) (@Some A phi3) *)
inversion H2; subst.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
(* Goal: or (@necR A H z c) (@necR A H c z) *)
right.
(* Goal: @necR A H c z *)
(* Goal: or (@necR A H z c) (@necR A H c z) *)
apply rt_trans with y.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
constructor 1; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
apply rt1n_trans; auto.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
unfold age in H0,H3.
(* Goal: or (@necR A H z c) (@necR A H c z) *)
rewrite H0 in H3; inv H3.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct (IHclos_refl_trans_1n _ H4); auto.
Qed.

Lemma necR_linear' {A} `{H : ageable A}:
   forall {a b c}, necR a b -> necR a c -> level b = level c -> b=c.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: @eq A b c *)
destruct (necR_linear H0 H1).
(* Goal: @eq A b c *)
(* Goal: @eq A b c *)
clear - H2 H3.
(* Goal: @eq A b c *)
apply nec_refl_or_later in H3.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H3; auto.
(* Goal: le n' m *)
apply laterR_level in H0; unfold fashionR in H2; elimtype False; omega.
(* Goal: @eq A b c *)
apply nec_refl_or_later in H3.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
destruct H3; auto.
(* Goal: le n' m *)
apply laterR_level in H3; unfold fashionR in H2; elimtype False; omega.
Qed.

Lemma laterR_necR {A} `{agA : ageable A}:
  forall {x y}, laterR x y -> necR x y.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
induction 1; intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
constructor; auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
econstructor 3; auto.
(* Goal: clos_refl_trans A (@age A agA) x z *)
apply rt_trans with y; auto.
Qed.

Lemma necR_refl {A} `{H : ageable A}:
  forall phi, necR phi phi.
Proof.
(* Goal: @necR A agA w' w' *)
(* Goal: @necR A agA w w' *)
intros; constructor 2.
Qed.

Hint Resolve @necR_refl.

Lemma necR_trans  {A} `{H : ageable A}:
  forall phi1 phi2 phi3, necR phi1 phi2 -> necR phi2 phi3 -> necR phi1 phi3.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
econstructor 3; eauto.
Qed.

Lemma necR_laterR {A} `{agA : ageable A}:
  forall w1 w2 w3, necR w1 w2 -> laterR w2 w3 -> laterR w1 w3.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
intros.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @necR A H phi1 phi2) (_ : @necR A H phi2 phi3), @necR A H phi1 phi3 *)
revert w3 H0; induction H; intros.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
econstructor 2. constructor 1; eauto. apply H0.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
(* Goal: @ex nat (fun i : nat => and (F i) (and (lt i n) (not (F (S i))))) *)
auto.
Qed.
