(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import List.
Require Extraction.

Inductive letter : Set :=
  | A : letter
  | B : letter.

Definition word := list letter.

Inductive emb : word -> word -> Prop :=
  | emb0 : forall ys : word, emb nil ys
  | emb1 :
      forall (xs ys : list letter) (y : letter),
      emb xs ys -> emb xs (y :: ys)
  | emb2 :
      forall (xs ys : list letter) (x : letter),
      emb xs ys -> emb (x :: xs) (x :: ys).

Inductive L (v : word) : list word -> Set :=
  | L0 : forall (w : word) (ws : list word), emb w v -> L v (w :: ws)
  | L1 : forall (w : word) (ws : list word), L v ws -> L v (w :: ws).

Inductive good : list word -> Set :=
  | good0 : forall (ws : list word) (w : word), L w ws -> good (w :: ws)
  | good1 : forall (ws : list word) (w : word), good ws -> good (w :: ws).

Inductive R (a : letter) : list word -> list word -> Set :=
  | R0 : R a nil nil
  | R1 :
      forall (vs ws : list word) (w : word),
      R a vs ws -> R a (w :: vs) ((a :: w) :: ws).

Inductive T (a : letter) : list word -> list word -> Set :=
  | T0 :
      forall (b : letter) (w : word) (ws zs : list word),
      a <> b -> R b ws zs -> T a (w :: zs) ((a :: w) :: zs)
  | T1 :
      forall (w : word) (ws zs : list word),
      T a ws zs -> T a (w :: ws) ((a :: w) :: zs)
  | T2 :
      forall (b : letter) (w : word) (ws zs : list word),
      a <> b -> T a ws zs -> T a ws ((b :: w) :: zs).

Inductive bar : list word -> Set :=
  | bar1 : forall ws : list word, good ws -> bar ws
  | bar2 : forall ws : list word, (forall w : word, bar (w :: ws)) -> bar ws.

Hint Constructors emb.
Hint Constructors L.
Hint Constructors good.
Hint Constructors R.
Hint Constructors T. 
Hint Constructors bar.
Hint Extern 5 (?X1 <> ?X2) => intro; discriminate.

Theorem prop1 : forall ws : list word, bar (nil :: ws).
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
auto.
Defined.
Hint Resolve prop1.

Theorem lemma1 :
 forall (ws : list word) (xs : word) (x : letter), L xs ws -> L (x :: xs) ws.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
simple induction 1; auto.
Defined.
Hint Resolve lemma1.

Theorem lemma2' :
 forall (vs ws : list word) (x : letter) (xs : word),
 R x vs ws -> L xs vs -> L (x :: xs) ws.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: forall (ws : list word) (w : word) (_ : R a (@nil word) ws) (_ : forall _ : not (@eq (list word) (@nil word) (@nil word)), T a (@nil word) ws) (_ : not (@eq (list word) (@cons word w (@nil word)) (@nil word))), T a (@cons word w (@nil word)) (@cons (list letter) (@cons letter a w) ws) *)
(* Goal: forall (w : word) (l ws : list word) (w0 : word) (_ : R a (@cons word w l) ws) (_ : forall _ : not (@eq (list word) (@cons word w l) (@nil word)), T a (@cons word w l) ws) (_ : not (@eq (list word) (@cons word w0 (@cons word w l)) (@nil word))), T a (@cons word w0 (@cons word w l)) (@cons (list letter) (@cons letter a w0) ws) *)
inversion 1.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
inversion 3; auto.
Defined.
Hint Resolve lemma2'.

Theorem lemma2 :
 forall (vs ws : list word) (a : letter), R a vs ws -> good vs -> good ws.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
simple induction 1; auto.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
inversion 3; eauto.
Defined.
Hint Resolve lemma2.

Theorem lemma3' :
 forall (vs ws : list word) (x : letter) (xs : word),
 T x vs ws -> L xs vs -> L (x :: xs) ws.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
simple induction 1; auto; inversion 3; auto.
Defined.
Hint Resolve lemma3'.

Theorem lemma3 :
 forall (ws zs : list word) (a : letter), T a ws zs -> good ws -> good zs.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
simple induction 1; auto; inversion 3; eauto.
Defined.
Hint Resolve lemma3.

Theorem lemma4 :
 forall (ws zs : list word) (a : letter), R a ws zs -> ws <> nil -> T a ws zs.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
tauto.
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro.
(* Goal: forall (ws : list word) (w : word) (_ : R a vs ws) (_ : forall _ : not (@eq (list word) vs (@nil word)), T a vs ws) (_ : not (@eq (list word) (@cons word w vs) (@nil word))), T a (@cons word w vs) (@cons (list letter) (@cons letter a w) ws) *)
case vs.
(* Goal: forall (ws : list word) (w : word) (_ : R a (@nil word) ws) (_ : forall _ : not (@eq (list word) (@nil word) (@nil word)), T a (@nil word) ws) (_ : not (@eq (list word) (@cons word w (@nil word)) (@nil word))), T a (@cons word w (@nil word)) (@cons (list letter) (@cons letter a w) ws) *)
(* Goal: forall (w : word) (l ws : list word) (w0 : word) (_ : R a (@cons word w l) ws) (_ : forall _ : not (@eq (list word) (@cons word w l) (@nil word)), T a (@cons word w l) ws) (_ : not (@eq (list word) (@cons word w0 (@cons word w l)) (@nil word))), T a (@cons word w0 (@cons word w l)) (@cons (list letter) (@cons letter a w0) ws) *)
inversion 1.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: T a (@cons word w (@nil word)) (@cons (list letter) (@cons letter a w) (@nil word)) *)
(* Goal: forall (w : word) (l ws : list word) (w0 : word) (_ : R a (@cons word w l) ws) (_ : forall _ : not (@eq (list word) (@cons word w l) (@nil word)), T a (@cons word w l) ws) (_ : not (@eq (list word) (@cons word w0 (@cons word w l)) (@nil word))), T a (@cons word w0 (@cons word w l)) (@cons (list letter) (@cons letter a w0) ws) *)
case a.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
apply (T0 A B w nil); auto.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
apply (T0 B A w nil); auto.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
auto.
Defined.
Hint Resolve lemma4.

Theorem letter_neq : forall a b c : letter, a <> b -> c <> a -> c = b.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
intros a b c; case a; case b; case c; tauto.
Qed.

Theorem letter_eq_dec : forall a b : letter, {a = b} + {a <> b}.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: sumbool (@eq letter a b) (not (@eq letter a b)) *)
decide equality.
Defined.

Theorem prop2 :
 forall (a b : letter) (xs : list word),
 a <> b ->
 bar xs ->
 forall ys : list word,
 bar ys -> forall zs : list word, T a xs zs -> T b ys zs -> bar zs.
(* Goal: forall (a b : letter) (xs : list word) (_ : not (@eq letter a b)) (_ : bar xs) (ys : list word) (_ : bar ys) (zs : list word) (_ : T a xs zs) (_ : T b ys zs), bar zs *)
intros a b xs neq.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
eauto.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (ys : list word) (_ : bar ys) (zs : list word) (_ : T a (@cons word w ws) zs) (_ : T b ys zs), bar zs) (ys : list word) (_ : bar ys) (zs : list word) (_ : T a ws zs) (_ : T b ys zs), bar zs *)
simple induction 3.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
eauto.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: bar (@nil word) *)
apply bar2.
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro.
(* Goal: bar (@cons word w zs) *)
case w.
(* Goal: bar (@cons word (@nil letter) zs) *)
(* Goal: forall (l : letter) (l0 : list letter), bar (@cons word (@cons letter l l0) zs) *)
apply prop1.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: bar (@cons word (@cons letter l l0) zs) *)
elim (letter_eq_dec l a).
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
intro; rewrite a0; eauto.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
intro; rewrite (letter_neq a b l neq b2); eauto.
Defined.
Hint Resolve prop2.

Theorem prop3 :
 forall (a : letter) (xs : list word),
 bar xs -> forall zs : list word, xs <> nil -> R a xs zs -> bar zs.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
eauto.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: bar (@nil word) *)
apply bar2.
(* Goal: forall w : word, bar (@cons word w zs) *)
simple induction w.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
auto.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: bar (@cons word (@cons letter a0 l) zs) *)
elim (letter_eq_dec a0 a).
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro. 
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
rewrite a1; eauto.
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
apply (prop2 a0 a (l :: zs) b0 H3 ws); eauto.
Defined.
Hint Resolve prop3.

Theorem higman : bar nil.
(* Goal: bar (@nil word) *)
apply bar2.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
simple induction w; eauto.
Defined.
Hint Resolve higman.

Inductive is_prefix (A : Set) : list A -> (nat -> A) -> Prop :=
  | is_prefix_nil : forall f : nat -> A, is_prefix A nil f
  | is_prefix_cons :
      forall (f : nat -> A) (x : A) (xs : list A),
      x = f (length xs) -> is_prefix A xs f -> is_prefix A (x :: xs) f.
Hint Constructors is_prefix.

Theorem L_idx :
 forall (f : nat -> word) (w : word) (ws : list word),
 L w ws -> is_prefix word ws f -> {i : nat | emb (f i) w /\ i < length ws}. 
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sig nat (fun j : nat => and (emb (f x) (f j)) (lt x j)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
exists (length ws0).
(* Goal: and (emb (f (@length word ws0)) w) (lt (@length word ws0) (@length word (@cons word w0 ws0))) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
inversion_clear H0.
(* Goal: and (emb (f x) (f (@length word ws0))) (lt x (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
split.
(* Goal: emb (f (@length word ws0)) w *)
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
rewrite H1 in e.
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: lt (@length word ws0) (@length word (@cons word w0 ws0)) *)
(* Goal: forall (w0 : word) (ws : list word) (_ : L w ws) (_ : forall _ : is_prefix word ws f, @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word ws)))) (_ : is_prefix word (@cons word w0 ws) f), @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws)))) *)
auto.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
cut (is_prefix word ws0 f).
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro.
(* Goal: @sig nat (fun i : nat => and (emb (f i) w) (lt i (@length word (@cons word w0 ws0)))) *)
(* Goal: is_prefix word ws0 f *)
elim (H0 H2).
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
exists x.
(* Goal: and (emb (f x) (f (@length word ws0))) (lt x (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
elim p.
(* Goal: and (emb (f x) (f (@length word ws0))) (lt x (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
split.
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: lt x (@length word (@cons word w0 ws0)) *)
(* Goal: is_prefix word ws0 f *)
apply (le_S (S x) (length ws0)).
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: is_prefix word ws0 f *)
inversion H1.
(* Goal: is_prefix word ws0 f *)
assumption.
Defined.

Theorem good_idx :
 forall (f : nat -> word) (ws : list word),
 good ws ->
 is_prefix word ws f -> {i : nat &  {j : nat | emb (f i) (f j) /\ i < j}}.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
elim (L_idx f w ws0 l).
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
exists x.
(* Goal: @sig nat (fun j : nat => and (emb (f x) (f j)) (lt x j)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
exists (length ws0).
(* Goal: and (emb (f x) (f (@length word ws0))) (lt x (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
elim p.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
inversion H0.
(* Goal: and (emb (f x) (f (@length word ws0))) (lt x (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
split.
(* Goal: emb (f x) (f (@length word ws0)) *)
(* Goal: lt x (@length word ws0) *)
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
rewrite H5 in H1.
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: is_prefix word ws0 f *)
(* Goal: forall (ws : list word) (w : word) (_ : good ws) (_ : forall _ : is_prefix word ws f, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
inversion H0.
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
cut (is_prefix word ws0 f).
(* Goal: is_prefix word ws0 f *)
assumption.
(* Goal: is_prefix word ws0 f *)
inversion H1.
(* Goal: is_prefix word ws0 f *)
assumption.
Defined.

Theorem bar_idx :
 forall (f : nat -> word) (ws : list word),
 bar ws ->
 is_prefix word ws f -> {i : nat &  {j : nat | emb (f i) (f j) /\ i < j}}.
(* Goal: forall (f : forall _ : nat, word) (ws : list word) (_ : bar ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
simple induction 1.
(* Goal: forall (ws : list word) (_ : good ws) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
apply good_idx.
(* Goal: forall (ws : list word) (_ : forall w : word, bar (@cons word w ws)) (_ : forall (w : word) (_ : is_prefix word (@cons word w ws) f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j)))) (_ : is_prefix word ws f), @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intros.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
apply (H0 (f (length ws0))).
(* Goal: is_prefix word (@cons word (f (@length word ws0)) ws0) f *)
apply is_prefix_cons.
(* Goal: @eq word (f (@length word ws0)) (f (@length word ws0)) *)
(* Goal: is_prefix word ws0 f *)
reflexivity.
(* Goal: is_prefix word ws0 f *)
assumption.
Defined.

Theorem higman_idx :
 forall f : nat -> word, {i : nat &  {j : nat | emb (f i) (f j) /\ i < j}}.
(* Goal: forall f : forall _ : nat, word, @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
intro.
(* Goal: @sigT nat (fun i : nat => @sig nat (fun j : nat => and (emb (f i) (f j)) (lt i j))) *)
apply (bar_idx f nil).
(* Goal: bar (@nil word) *)
(* Goal: is_prefix word (@nil word) f *)
apply higman.
(* Goal: is_prefix word (@nil word) f *)
apply is_prefix_nil.
Defined.

Extraction NoInline lemma1.
Extraction "higman2.ml" higman_idx.
