Require Import PArith List ChoiceFacts Omega.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool.

Require Import Classes RandomQC GenLow Sets.
Import GenLow.

Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Goal: not (@eq nat m O) *)
(* LL: TODO: Add proof obligation that the result paths be prefix free? *)
Class CoArbitrary (A : Type) : Type :=
  {
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    coarbitrary : A -> positive;
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    coarbReverse : positive -> option A;
    coarbCorrect : forall a, coarbReverse (coarbitrary a) = Some a
  }.

Instance coArbPos : CoArbitrary positive.
Proof.
refine {|
    coarbitrary x := x;
    coarbReverse x := Some x
  |}.
(* Goal: Pos.le p max *)
auto.
Qed.

Lemma nat_lemma :   forall a : nat,
  Some (Init.Nat.pred (Pos.to_nat (Pos.of_nat (S a)))) = Some a.
Admitted.

Instance coqArbNat : CoArbitrary nat.
Proof.
refine {|
    coarbitrary x := Pos.of_nat (S x);
    coarbReverse p := Some (Coq.Init.Peano.pred (Pos.to_nat p))
  |}.
(* Goal: forall a : nat, @eq (option nat) (@Some nat (Init.Nat.pred (Pos.to_nat (Pos.of_nat (S a))))) (@Some nat a) *)
  apply nat_lemma.
Qed.

Local Open Scope positive.
Fixpoint posToPathAux (p : positive) : SplitPath := 
  match p with 
    | xH => []
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    | xI p' => posToPathAux p' ++ [Left; Right]
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    | xO p' => posToPathAux p' ++ [Left; Left ]
  end.

Definition posToPath (p : positive) : SplitPath := posToPathAux p ++ [Right].

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Fixpoint pathToPosAux (p : SplitPath) (f : positive -> positive) 
: option positive :=
match p with 
  | [Right] => Some (f xH)
  | Left :: Right :: p' => pathToPosAux p' (fun p => xI (f p))
  | Left :: Left  :: p' => pathToPosAux p' (fun p => xO (f p))     
  | _ => None
end.

Definition pathToPos p := pathToPosAux p (fun x => x).

(* Goal: not (@eq nat m O) *)
(*
Eval compute in (pathToPos (posToPath 1)).
Eval compute in (pathToPos (posToPath 2)).
Eval compute in (pathToPos (posToPath 3)).
Eval compute in (pathToPos (posToPath 4)).
Eval compute in (pathToPos (posToPath 5)).
Eval compute in (pathToPos (posToPath 6)).
Eval compute in (pathToPos (posToPath 7)).
Eval compute in (pathToPos (posToPath 8)).
Eval compute in (pathToPos (posToPath 9)).
(* Goal: not (@eq nat m O) *)
*)

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Definition list_ind' (A : Type) (P : list A -> Prop) : 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                    P [] -> (forall (a : A), P [a]) -> 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                    (forall (a b : A) (l : list A), P l -> P (a :: b :: l)) ->
                    forall (l : list A), P l :=
  fun H0 H1 H2 => 
    fix aux (l : list A) : P l := 
      match l with 
        | []  => H0
        | [x] => H1 x
        | a :: b :: l' => H2 a b l' (aux l')
      end.

(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
Lemma aux1 : forall l p f, pathToPosAux (l ++ [Right]) f = Some p ->
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
               exists f', forall l', pathToPosAux (l ++ l') f =
                                    pathToPosAux l' f' /\ f' xH = p.
(* Goal: forall (l : list SplitDirection) (p : positive) (f : forall _ : positive, positive) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection l (@cons SplitDirection Right (@nil SplitDirection))) f) (@Some positive p)), @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') f) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
induction l using list_ind'; intros.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ simpl in *; inversion H; subst.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux l' f) (pathToPosAux l' f')) (@eq positive (f' xH) (f xH))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@nil SplitDirection)) l') f) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) l') f) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
  exists f; intros.
(* Goal: Pos.le p max *)
  split; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ simpl in H; destruct a; inversion H.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ pose proof IHl p; clear IHl.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) l') f) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
  destruct a; destruct b; simpl in *.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  -  pose proof (H0 (fun p0 => xO (f p0))); clear H0.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
     apply H1 in H; clear H1.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
     assumption.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  -  pose proof (H0 (fun p0 => xI (f p0))); clear H0.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
     apply H1 in H; clear H1.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
     assumption.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion H.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion H.
Qed.

Lemma posPathInj : forall p, pathToPos (posToPath p) = Some p.
(* Goal: forall p : positive, @eq (option positive) (pathToPos (posToPath p)) (@Some positive p) *)
induction p; unfold posToPath, pathToPos in *; simpl in *.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
- apply aux1 in IHp. 
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@nil SplitDirection)))) (@cons SplitDirection Right (@nil SplitDirection))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  inversion IHp as [f' Hyp]; clear IHp.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  rewrite <- app_assoc; simpl.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Right (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xI p)) *)
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@nil SplitDirection)))) (@cons SplitDirection Right (@nil SplitDirection))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  pose proof Hyp [Left; Right; Right] as H; clear Hyp.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  inversion H as [H0 H1]; clear H.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  rewrite H0; clear H0.
(* Goal: Pos.le p max *)
  simpl; subst; auto.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
- apply aux1 in IHp. 
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@nil SplitDirection)))) (@cons SplitDirection Right (@nil SplitDirection))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  inversion IHp as [f' Hyp]; clear IHp.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  rewrite <- app_assoc; simpl.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  pose proof Hyp [Left; Left; Right] as H; clear Hyp.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  inversion H as [H0 H1]; clear H.
(* Goal: @eq (option positive) (pathToPosAux (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@cons SplitDirection Right (@nil SplitDirection))))) (fun x : positive => x)) (@Some positive (xO p)) *)
(* Goal: @eq (option positive) (@Some positive xH) (@Some positive xH) *)
  rewrite H0; clear H0.
(* Goal: Pos.le p max *)
  simpl; subst; auto.
(* Goal: Pos.le p max *)
- auto.
Qed.

(* Goal: not (@eq nat m O) *)
Fixpoint lengthSplit {A : Type} (l l' : list A) : option (list A * list A) :=
  match l, l' with
    | [], x => Some ([], x)
    | _::xs, y::ys => 
(* Goal: not (@eq nat m O) *)
      option_map (fun (p : list A * list A) => 
                    let (l1,l2) := p in (y::l1, l2)) (lengthSplit xs ys)
    | _, _ => None
  end.

Lemma lengthSplit1 : forall {A : Type} (l l' : list A), 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                       le (length l) (length l') -> 
                       exists p, lengthSplit l l' = Some p.
(* Goal: forall (A : Type) (l l' l1 l2 : list A) (_ : @eq (option (prod (list A) (list A))) (@lengthSplit A l l') (@Some (prod (list A) (list A)) (@pair (list A) (list A) l1 l2))), @eq nat (@length A l1) (@length A l) *)
induction l as [ | x xs IHxs].
(* Goal: Pos.le p max *)
+ intros; exists ([], l'); auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros l' LE; destruct l' as [ | b bs] eqn:LEq.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion LE.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - pose proof IHxs bs as IH; clear IHxs.
    assert (LE' : le (length xs) (length bs))
(* Goal: not (@eq nat m O) *)
           by (simpl in *; omega). (* Overkill? :) *)
(* Goal: @ex (prod (list A) (list A)) (fun p : prod (list A) (list A) => @eq (option (prod (list A) (list A))) (@lengthSplit A (@cons A x xs) (@cons A b bs)) (@Some (prod (list A) (list A)) p)) *)
    clear LE.
(* Goal: @ex (prod (list A) (list A)) (fun p : prod (list A) (list A) => @eq (option (prod (list A) (list A))) (@lengthSplit A (@cons A x xs) (@cons A b bs)) (@Some (prod (list A) (list A)) p)) *)
    apply IH in LE'; clear IH.
(* Goal: @ex (prod (list A) (list A)) (fun p : prod (list A) (list A) => @eq (option (prod (list A) (list A))) (@lengthSplit A (@cons A x xs) (@cons A b bs)) (@Some (prod (list A) (list A)) p)) *)
    inversion LE' as [pair Split]; clear LE'.
(* Goal: @ex (prod (list A) (list A)) (fun p : prod (list A) (list A) => @eq (option (prod (list A) (list A))) (@lengthSplit A (@cons A x xs) (@cons A b bs)) (@Some (prod (list A) (list A)) p)) *)
    destruct pair as [l1 l2] eqn:Pair.
(* Goal: @In nat n (rangeNat (S m)) *)
    simpl.
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
    rewrite Split.
(* Goal: @ex (prod (list A) (list A)) (fun p : prod (list A) (list A) => @eq (option (prod (list A) (list A))) (@option_map (prod (list A) (list A)) (prod (list A) (list A)) (fun p0 : prod (list A) (list A) => let (l1, l2) := p0 in @Datatypes.pair (list A) (list A) (@cons A b l1) l2) (@Some (prod (list A) (list A)) (@Datatypes.pair (list A) (list A) l1 l2))) (@Some (prod (list A) (list A)) p)) *)
    exists (b :: l1, l2).
(* Goal: @In nat n (rangeNat (S m)) *)
    simpl.
(* Goal: Pos.le p max *)
    auto.
Qed.

Lemma lengthSplit2 : forall {A : Type} (l l' l1 l2 : list A), 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                       lengthSplit l l' = Some (l1, l2) -> l1 ++ l2 = l'.
(* Goal: forall (A : Type) (l l' l1 l2 : list A) (_ : @eq (option (prod (list A) (list A))) (@lengthSplit A l l') (@Some (prod (list A) (list A)) (@pair (list A) (list A) l1 l2))), @eq (list A) (@app A l1 l2) l' *)
induction l.
(* Goal: Pos.le p max *)
+ intros l' l1 l2 Hyp; simpl in Hyp; inversion_clear Hyp; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros l' l1 l2 Hyp. 
(* Goal: @eq (list A) (@app A l1 l2) l' *)
  simpl in Hyp.
(* Goal: @eq (list A) (@app A l1 l2) l' *)
  destruct l' as [ | y ys] eqn:L'.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion Hyp.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - destruct l1 eqn:L1.
(* Goal: not (@eq nat m O) *)
    * destruct (lengthSplit l ys); simpl in *.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + destruct p; congruence.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + congruence.
(* Goal: not (@eq nat m O) *)
    * pose proof IHl ys l0 l2; clear IHl.
(* Goal: not (@eq nat m O) *)
      destruct (lengthSplit l ys) eqn:LenSplit; simpl in *.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + inversion Hyp. destruct p. inversion H1. subst.
(* Goal: Pos.le p max *)
        rewrite H; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + inversion Hyp.
Qed.      

Lemma lengthSplit3 : forall {A : Type} (l l' l1 l2 : list A), 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                       lengthSplit l l' = Some (l1, l2) -> length l1 = length l.
(* Goal: forall (A : Type) (l l' l1 l2 : list A) (_ : @eq (option (prod (list A) (list A))) (@lengthSplit A l l') (@Some (prod (list A) (list A)) (@pair (list A) (list A) l1 l2))), @eq nat (@length A l1) (@length A l) *)
induction l as [ | x xs IHxs].
(* Goal: Pos.le p max *)
+ intros; simpl in H; inversion H; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros l' l1 l2 Split.
(* Goal: @eq nat (@length A l1) (@length A (@cons A x xs)) *)
  simpl in Split.
(* Goal: @eq nat (@length A l1) (@length A (@cons A x xs)) *)
  destruct l'.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion Split.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - destruct l1.
(* Goal: not (@eq nat m O) *)
    * destruct (lengthSplit xs l').
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + simpl in *. destruct p. inversion Split.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + simpl in *. inversion Split.
(* Goal: not (@eq nat m O) *)
    * simpl in *. 
(* Goal: @eq nat (S (@length A l1)) (S (@length A xs)) *)
      destruct (lengthSplit xs l') eqn:LenSplit.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + simpl in *. destruct p. inversion Split; subst; clear Split.
(* Goal: @eq nat (S (@length A l1)) (S (@length A xs)) *)
(* Goal: @eq nat (S (@length A l1)) (S (@length A xs)) *)
        pose proof (IHxs l' l1 l2 LenSplit) as Hyp; clear IHxs.
(* Goal: Pos.le p max *)
        auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      + simpl in *. inversion Split.
Qed.        

(* Goal: not (@eq nat m O) *)
Lemma lengthPathEven : forall p, exists n, length (posToPathAux p) = (2 * n)%nat.
(* Goal: forall p : positive, @ex nat (fun n : nat => @eq nat (@length SplitDirection (posToPathAux p)) (Init.Nat.mul (S (S O)) n)) *)
induction p.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ inversion IHp as [n Hyp]; clear IHp.
(* Goal: @In nat n (rangeNat (S m)) *)
  simpl.
(* Goal: @ex nat (fun n : nat => @eq nat (@length SplitDirection (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@nil SplitDirection))))) (Init.Nat.add n (Init.Nat.add n O))) *)
(* Goal: @ex nat (fun n : nat => @eq nat (@length SplitDirection (posToPathAux xH)) (Init.Nat.mul (S (S O)) n)) *)
  exists (S n).
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
  rewrite app_length. 
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
  rewrite Hyp.
(* Goal: @In nat n (rangeNat (S m)) *)
  simpl.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) match a with | Left => match l' with | nil => @None positive | cons (Left as s) p' => pathToPosAux p' (fun p : positive => xO (f p)) | cons (Right as s) p' => pathToPosAux p' (fun p : positive => xI (f p)) end | Right => match l' with | nil => @Some positive (f xH) | cons s l => @None positive end end (pathToPosAux l' f')) (@eq (option positive) match a with | Left => match @app SplitDirection l' lApp with | nil => @None positive | cons (Left as s) p' => pathToPosAux p' (fun p : positive => xO (f p)) | cons (Right as s) p' => pathToPosAux p' (fun p : positive => xI (f p)) end | Right => match @app SplitDirection l' lApp with | nil => @Some positive (f xH) | cons s l => @None positive end end (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: forall (l' l'' lApp : list SplitDirection) (f : forall _ : positive, positive) (n : nat) (p : positive) (_ : @eq nat (@length SplitDirection (@cons SplitDirection a (@cons SplitDirection b l))) (Init.Nat.mul (S (S O)) n)) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) (@app SplitDirection l' l'')) f) (@Some positive p)), @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) l') f) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) (@app SplitDirection l' lApp)) f) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
  omega.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ inversion IHp as [n Hyp]; clear IHp.
(* Goal: @In nat n (rangeNat (S m)) *)
  simpl.
(* Goal: @ex nat (fun n : nat => @eq nat (@length SplitDirection (@app SplitDirection (posToPathAux p) (@cons SplitDirection Left (@cons SplitDirection Left (@nil SplitDirection))))) (Init.Nat.add n (Init.Nat.add n O))) *)
(* Goal: @ex nat (fun n : nat => @eq nat (@length SplitDirection (posToPathAux xH)) (Init.Nat.mul (S (S O)) n)) *)
  exists (S n).
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
  rewrite app_length. 
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
  rewrite Hyp.
(* Goal: @In nat n (rangeNat (S m)) *)
  simpl.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) match a with | Left => match l' with | nil => @None positive | cons (Left as s) p' => pathToPosAux p' (fun p : positive => xO (f p)) | cons (Right as s) p' => pathToPosAux p' (fun p : positive => xI (f p)) end | Right => match l' with | nil => @Some positive (f xH) | cons s l => @None positive end end (pathToPosAux l' f')) (@eq (option positive) match a with | Left => match @app SplitDirection l' lApp with | nil => @None positive | cons (Left as s) p' => pathToPosAux p' (fun p : positive => xO (f p)) | cons (Right as s) p' => pathToPosAux p' (fun p : positive => xI (f p)) end | Right => match @app SplitDirection l' lApp with | nil => @Some positive (f xH) | cons s l => @None positive end end (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: forall (l' l'' lApp : list SplitDirection) (f : forall _ : positive, positive) (n : nat) (p : positive) (_ : @eq nat (@length SplitDirection (@cons SplitDirection a (@cons SplitDirection b l))) (Init.Nat.mul (S (S O)) n)) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) (@app SplitDirection l' l'')) f) (@Some positive p)), @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) l') f) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) (@app SplitDirection l' lApp)) f) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
  omega.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ exists (O).
(* Goal: @In nat n (rangeNat (S m)) *)
  simpl.
(* Goal: Pos.le p max *)
  auto.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma evenPathAux : forall l l' l'' lApp f n p, length l = (2 * n)%nat -> 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                      pathToPosAux (l ++ l' ++ l'') f = Some p ->
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                      exists f', pathToPosAux (l ++ l') f = pathToPosAux l' f'
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                                 /\ pathToPosAux (l ++ l' ++ lApp) f = 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                                    pathToPosAux (l' ++ lApp) f'.
(* Goal: forall (l l' l'' lApp : list SplitDirection) (f : forall _ : positive, positive) (n : nat) (p : positive) (_ : @eq nat (@length SplitDirection l) (Init.Nat.mul (S (S O)) n)) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' l'')) f) (@Some positive p)), @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') f) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) f) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
induction l using list_ind'.
(* Goal: Pos.le p max *)
+ intros. exists f. auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros. simpl in *. omega.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros l' l'' lApp f n p Len Valid.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) l') f) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection (@cons SplitDirection a (@cons SplitDirection b l)) (@app SplitDirection l' lApp)) f) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
  destruct n.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - simpl in Len. congruence.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - simpl in Len; assert (length l = (2 * n)%nat) by omega.
(* Goal: not (@eq nat m O) *)
    destruct a eqn:A; destruct b eqn:B; simpl in *.
(* Goal: not (@eq nat m O) *)
    * unfold pathToPos in Valid. simpl in Valid.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xO (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xO (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      pose proof (IHl l' l'' lApp (fun p => xO (f p)) n p H Valid) as Hyp; clear IHl H.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      inversion Hyp as [f' HF]; clear Hyp.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      exists f'.
(* Goal: Pos.le p max *)
      auto.
(* Goal: not (@eq nat m O) *)
    * unfold pathToPos in Valid. simpl in Valid.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      pose proof (IHl l' l'' lApp (fun p => xI (f p)) n p H Valid) as Hyp; clear IHl H.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      inversion Hyp as [f' HF]; clear Hyp.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq (option positive) (pathToPosAux (@app SplitDirection l (@app SplitDirection l' lApp)) (fun p : positive => xI (f p))) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq (option positive) (@None positive) (pathToPosAux (@app SplitDirection l' lApp) f'))) *)
      exists f'.
(* Goal: Pos.le p max *)
      auto.
(* Goal: not (@eq nat m O) *)
    * inversion Valid.
(* Goal: not (@eq nat m O) *)
    * inversion Valid.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma pathBeginsLeft : forall l1 l2 f x, l1 <> [] -> l2 <> [] -> 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                                     pathToPosAux (l1 ++ l2) f = Some x ->
                                     head l1 = Some Left.
(* Goal: forall (l1 l2 : list SplitDirection) (f : forall _ : positive, positive) (x : positive) (_ : not (@eq (list SplitDirection) l1 (@nil SplitDirection))) (_ : not (@eq (list SplitDirection) l2 (@nil SplitDirection))) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection l1 l2) f) (@Some positive x)), @eq (option SplitDirection) (@hd_error SplitDirection l1) (@Some SplitDirection Left) *)
destruct l1.
(* Goal: Pos.le p max *)
+ intros. exfalso; apply H; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros. 
(* Goal: @eq (option SplitDirection) (@hd_error SplitDirection (@cons SplitDirection s l1)) (@Some SplitDirection Left) *)
  destruct s.
(* Goal: Pos.le p max *)
  - auto.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - simpl in H1. 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    destruct (l1 ++ l2) eqn:Contra.
(* Goal: not (@eq nat m O) *)
    * destruct l1; destruct l2; try solve [unfold not; exfalso; auto]; 
(* Goal: not (@eq nat m O) *)
      simpl in *; congruence.
(* Goal: not (@eq nat m O) *)
    * congruence.
Qed.

Lemma listAppNeq : forall (A : Type) (l1 l2 l3 l4 : list A), 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                     (forall (x y : A), {x = y} + {x <> y}) ->
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                     length l1 = length l2 -> 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                     l1 <> l2 ->
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
                     l1 ++ l3 <> l2 ++ l4.
(* Goal: forall (A : Type) (l1 l2 l3 l4 : list A) (_ : forall x y : A, sumbool (@eq A x y) (not (@eq A x y))) (_ : @eq nat (@length A l1) (@length A l2)) (_ : not (@eq (list A) l1 l2)), not (@eq (list A) (@app A l1 l3) (@app A l2 l4)) *)
induction l1.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros.
(* Goal: not (@eq (list A) (@app A (@nil A) l3) (@app A l2 l4)) *)
(* Goal: forall (l2 l3 l4 : list A) (_ : forall x y : A, sumbool (@eq A x y) (not (@eq A x y))) (_ : @eq nat (@length A (@cons A a l1)) (@length A l2)) (_ : not (@eq (list A) (@cons A a l1) l2)), not (@eq (list A) (@app A (@cons A a l1) l3) (@app A l2 l4)) *)
  destruct l2.
(* Goal: Pos.le p max *)
  - unfold not in H0. exfalso; apply H0; auto.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - simpl in H; inversion H.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros l2 l3 l4 EqDec Len Neq.
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A l2 l4)) *)
  destruct l2 as [ | b l2 ].
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - simpl in Len. congruence.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - destruct (EqDec a b).
(* Goal: not (@eq nat m O) *)
    * subst. simpl in Len. 
(* Goal: not (@eq (list A) (@app A (@cons A b l1) l3) (@app A (@cons A b l2) l4)) *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      inversion Len as [ Len']; clear Len.
(* Goal: @In nat n (rangeNat (S m)) *)
      simpl.
(* Goal: not (@eq (list A) (@cons A b (@app A l1 l3)) (@cons A b (@app A l2 l4))) *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      pose proof (IHl1 l2 l3 l4 EqDec Len') as Contra; clear IHl1.
(* Goal: not (@eq (list A) (@cons A b (@app A l1 l3)) (@cons A b (@app A l2 l4))) *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      assert (l1 <> l2) by (unfold not; intros; congruence).
(* Goal: not (@eq (list A) (@cons A b (@app A l1 l3)) (@cons A b (@app A l2 l4))) *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      apply Contra in H.
(* Goal: not (@eq nat m O) *)
      unfold not in *.
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
      intros.
(* Goal: False *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      apply H.
(* Goal: @eq (list A) (@app A l1 l3) (@app A l2 l4) *)
(* Goal: not (@eq (list A) (@app A (@cons A a l1) l3) (@app A (@cons A b l2) l4)) *)
      inversion H0.
(* Goal: Pos.le p max *)
      auto.
(* Goal: not (@eq nat m O) *)
    * unfold not; intros.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      inversion H.
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      congruence.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma PosToPathPrefixFreeAux : forall (x y : positive), (x <> y) -> 
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                                 le (length (posToPathAux y)) (length(posToPathAux x)) ->
                              PrefixFree [posToPath x;
                                          posToPath y].
intros x y H Leq.
apply FreeCons; [ apply FreeCons ; [ constructor | intros p Contra; inversion Contra] | ].
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros.
inversion H0; subst; clear H0; [ | inversion H2].
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
unfold posToPath in *; simpl in *; repeat rewrite <- app_assoc in *.

pose proof (lengthSplit1 Leq) as Hyp.
inversion Hyp as [pair Split]; clear Hyp.
destruct pair as [l0 l1].
pose proof (lengthSplit2 Split) as AppHyp.
pose proof (lengthSplit3 Split) as LenHyp.
pose proof (lengthPathEven y) as Hyp; inversion Hyp as [n LenN]; subst; clear Hyp.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
assert (XHyp : pathToPosAux (l0 ++ l1 ++ [Right]) (fun x => x) = Some x); 
  [ rewrite app_assoc; rewrite AppHyp; apply posPathInj | ].

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
rewrite <- LenHyp in LenN.

pose proof (evenPathAux [Right] LenN XHyp) as Even.
inversion Even as [f' HF]; clear Even.
inversion HF as [HF1 HF2]; clear HF.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
rewrite <- AppHyp in H1.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
rewrite <- app_assoc in H1.

destruct (list_eq_dec Direction_eq_dec (posToPathAux y) l0).
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
- subst. apply app_inv_head in H1.
(* Goal: forall (l1 l2 : list SplitDirection) (f : forall _ : positive, positive) (x : positive) (_ : not (@eq (list SplitDirection) l1 (@nil SplitDirection))) (_ : not (@eq (list SplitDirection) l2 (@nil SplitDirection))) (_ : @eq (option positive) (pathToPosAux (@app SplitDirection l1 l2) f) (@Some positive x)), @eq (option SplitDirection) (@hd_error SplitDirection l1) (@Some SplitDirection Left) *)
  destruct l1.
(* Goal: not (@eq nat m O) *)
  *  simpl in AppHyp; rewrite app_nil_r in AppHyp.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
      assert (posToPathAux y ++ [Right] = posToPathAux x ++ [Right]) 
        by (rewrite AppHyp; auto).
      assert (posToPath y = posToPath x) by (unfold posToPath; auto).
      assert (pathToPos (posToPath y) = pathToPos (posToPath x)) by (rewrite H2; auto).
      repeat rewrite posPathInj in H3.
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      congruence.
(* Goal: not (@eq nat m O) *)
  * assert (Contra : hd_error (s :: l1) = Some Left).
    eapply pathBeginsLeft.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    + unfold not; intros; congruence.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    + instantiate (1 := [Right]); unfold not; intros; congruence.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    + instantiate (1:= x); instantiate (1:=f').
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      rewrite <- HF2.
      apply XHyp.
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    simpl in Contra. inversion Contra; subst. simpl in H1. congruence.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
- eapply listAppNeq.
(* Goal: not (@eq nat m O) *)
  * apply Direction_eq_dec.
(* Goal: Pos.le p max *)
  * instantiate (1 := l0). instantiate (1 := posToPathAux y). eauto.
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (pathToPosAux (@app SplitDirection l l') (fun p : positive => xI (f p))) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
(* Goal: @ex (forall _ : positive, positive) (fun f' : forall _ : positive, positive => forall l' : list SplitDirection, and (@eq (option positive) (@None positive) (pathToPosAux l' f')) (@eq positive (f' xH) p)) *)
  * eassumption.
(* Goal: not (@eq nat m O) *)
  * eapply H1.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma prefixFreeCommutative : forall l1 l2, PrefixFree [l1;l2] -> PrefixFree [l2;l1].
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
inversion H.
apply FreeCons.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ apply FreeCons.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - constructor.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - intros. inversion H4.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ intros.
(* Goal: lt m (S (S n)) *)
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  subst.
  eapply H3.
(* Goal: Pos.le p max *)
  - instantiate (1 := l2); left; auto.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion H4.
(* Goal: not (@eq nat m O) *)
    * subst. inversion H4. subst. instantiate (1:= p1); instantiate (1 := p2).
(* Goal: Pos.le p max *)
      auto.
(* Goal: not (@eq nat m O) *)
    * inversion H0.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - inversion H0.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma PosToPathPrefixFree : forall (x y : positive), (x <> y) -> 
                              PrefixFree [posToPath x;
                                          posToPath y].
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros. 
destruct (Compare_dec.le_ge_dec (length (posToPathAux y)) 
                                (length (posToPathAux x))).
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ apply (PosToPathPrefixFreeAux H l).
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ apply prefixFreeCommutative.
(* Goal: PrefixFree (@cons SplitPath (posToPath y) (@cons SplitPath (posToPath x) (@nil SplitPath))) *)
  apply (@PosToPathPrefixFreeAux y x).
(* Goal: Pos.le p max *)
  - unfold not in *; intros; exfalso; auto.
(* Goal: Pos.le p max *)
  - auto.
Qed.

Function rangeNat (p : nat) : list nat :=
  match p with 
    | O => []
    | S n' => p :: (rangeNat n')
  end.

Definition rangePos (p : positive) : list positive := 
  map Pos.of_nat (rangeNat (Pos.to_nat p)).

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma ltInRange : forall m n, le n m -> n <> O -> In n (rangeNat m).
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
  induction m; intros.
(* Goal: Pos.le p max *)
  + inversion H. simpl. auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
  + simpl. inversion H.
(* Goal: Pos.le p max *)
    - left; auto.
(* Goal: Pos.le p max *)
    - right; subst. apply IHm; auto.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma posLtInRange : forall max pos, Pos.le pos max -> In pos (rangePos max).
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
  intros.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
  apply in_map_iff.
(* Goal: @ex nat (fun x : nat => and (@eq positive (Pos.of_nat x) pos) (@In nat x (rangeNat (Pos.to_nat max)))) *)
  exists (Pos.to_nat pos).
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  split.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - apply Pos2Nat.id.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  - apply ltInRange.
(* Goal: Pos.le p max *)
    + apply Pos2Nat.inj_le; auto.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
    + pose proof (Pos2Nat.is_succ pos) as Contra; inversion_clear Contra; congruence.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Lemma rangeNatLt : forall n m, In m (rangeNat n) -> lt m (S n) /\ m <> O.
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
  induction n; intros.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
  + simpl in H. inversion H. 
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
  + inversion H.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    - split. 
(* Goal: not (@eq nat m O) *)
      * subst. unfold lt. apply le_n.
(* Goal: not (@eq nat m O) *)
      * congruence.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    - apply IHn in H0; inversion H0; clear H0; split.
(* Goal: not (@eq nat m O) *)
      * unfold lt in *.
(* Goal: le (S m) (S (S n)) *)
(* Goal: not (@eq nat m O) *)
        apply le_S.
(* Goal: Pos.le p max *)
        auto.
(* Goal: Pos.le p max *)
      * auto.
Qed.    

Lemma rangePosPrefixFree : forall p, PrefixFree (map posToPath (rangePos p)).
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
  intros.
  unfold rangePos.
  induction (Pos.to_nat p) as [ | n IHn].
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
  + constructor.
(* Goal: Pos.le p max *)
  + simpl. apply FreeCons; auto.
    intros p' InP' p1 p2 App.
    apply in_map_iff in InP'.
    clear IHn.
    inversion InP' as [x xHyp]; clear InP'.
    inversion xHyp as [Pos2Path InX]; clear xHyp.
(* Goal: lt m (S (S n)) *)
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
    subst.
    apply in_map_iff in InX.
    inversion InX as [y yHyp]; clear InX.
    inversion yHyp as [Pos2PathY InY]; clear yHyp.
    apply rangeNatLt in InY.
    inversion InY as [LtYSn YNotO]; clear InY.
    remember (match n with | O => 1 | S _ => Pos.succ (Pos.of_nat n) end) as m.
    assert (Neq : x <> m).
(* Goal: lt m (S (S n)) *)
(* Goal: not (@eq nat m O) *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      unfold not; intros; subst.
      destruct y.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      - congruence.
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
      - destruct n.
(* Goal: not (@eq nat m O) *)
        * omega.
(* Goal: not (@eq nat m O) *)
        * assert (Pos.to_nat (Pos.of_nat (S y)) = Pos.to_nat (Pos.succ (Pos.of_nat (S n))))
            by (rewrite H; auto).
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
          rewrite Pos2Nat.inj_succ in H0.
          
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
          rewrite Nat2Pos.id in H0.
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
          rewrite Nat2Pos.id in H0.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
          + subst; omega.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
          + congruence.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
          + congruence.
    pose proof (@PosToPathPrefixFree x m) as Hyp.
    apply Hyp in Neq; clear Hyp.
    inversion Neq.
    eapply H2.
(* Goal: Pos.le p max *)
    + left; auto.
(* Goal: Pos.le p max *)
    + eauto.
Qed.    

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Definition posFunToPathFun (f : positive -> RandomSeed) (p : SplitPath) 
: RandomSeed :=
  match pathToPos p with 
    | Some a => f a
    | None   => newRandomSeed
  end.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Theorem coarbComplete' : forall (max : positive) (f : positive -> RandomSeed) ,
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                          exists seed, forall p, p <= max -> 
                            varySeed (posToPath p) seed = f p.
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros.
pose proof (SplitPathCompleteness (map posToPath (rangePos max)) 
                                (posFunToPathFun f) (rangePosPrefixFree max)).
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (p : positive) (_ : Pos.le p max), @eq RandomSeed (varySeed (posToPath p) seed) (f p)) *)
inversion H; clear H.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (p : positive) (_ : Pos.le p max), @eq RandomSeed (varySeed (posToPath p) seed) (f p)) *)
exists x.
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros.
(* Goal: @eq RandomSeed (varySeed (posToPath p) x) (f p) *)
pose proof H0 (posToPath p).
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
rewrite H1.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ unfold posFunToPathFun.
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
  rewrite posPathInj.
(* Goal: @eq RandomSeed (f a) (f a) *)
  reflexivity.
(* Goal: @In SplitPath (posToPath p) (@map positive SplitPath posToPath (rangePos max)) *)
+ apply in_map_iff.
(* Goal: @ex positive (fun x : positive => and (@eq SplitPath (posToPath x) (posToPath p)) (@In positive x (rangePos max))) *)
  exists p.
(* Goal: Pos.le p max *)
  split; auto.
(* Goal: @In positive p (rangePos max) *)
  apply posLtInRange.
(* Goal: Pos.le p max *)
  auto.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Definition funToPosFun {A : Type} `{_ : CoArbitrary A} (f : A -> RandomSeed) (p : positive)
: RandomSeed :=
  match coarbReverse p with 
    | Some a => f a
    | None   => newRandomSeed
  end.

Definition coarbLe {A : Type} `{_ : CoArbitrary A} (x y : A) : Prop :=
  Pos.le (coarbitrary x) (coarbitrary y).

Lemma coarbLePreservesLe : forall {A : Type} `{_ : CoArbitrary A} (x y : A),
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  coarbLe x y -> Pos.le (coarbitrary x) (coarbitrary y).
(* Goal: forall a : A, @ex RandomSeed (fun seed : RandomSeed => @eq B (@run B (@arbitrary B H0) s seed) (f a)) *)
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
by [].
Qed.

Theorem coarbComplete : forall {A : Type} `{_ : CoArbitrary A} (max : A)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                               (f : A -> RandomSeed),
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
                          exists seed, forall a, coarbLe a max ->
                                          varySeed (posToPath (coarbitrary a)) seed = f a.
(* Goal: forall (A : Type) (H : CoArbitrary A) (max : A) (f : forall _ : A, RandomSeed), @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
intros.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
pose proof (coarbComplete' (coarbitrary max) (funToPosFun f)) as Hyp.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
inversion Hyp as [seed HSeed]; clear Hyp.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
exists seed.
(* Goal: forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a) *)
intros a HLe.
(* Goal: @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a) *)
pose proof (HSeed (coarbitrary a)) as HCo; clear HSeed.
(* Goal: @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a) *)
apply coarbLePreservesLe in HLe.
(* Goal: @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a) *)
apply HCo in HLe; clear HCo.
(* Goal: @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a) *)
rewrite HLe; clear HLe.
(* Goal: @eq RandomSeed (@funToPosFun A H f (@coarbitrary A H a)) (f a) *)
unfold funToPosFun.
(* Goal: @eq RandomSeed match @coarbReverse A H (@coarbitrary A H a) with | Some a => f a | None => newRandomSeed end (f a) *)
rewrite coarbCorrect.
(* Goal: @eq RandomSeed (f a) (f a) *)
reflexivity.
Qed.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Instance genFun {A B : Type} `{_ : CoArbitrary A} `{_ : Gen B} : Gen (A -> B) :=
  {|
    arbitrary := 
      reallyUnsafePromote (fun a => variant (posToPath (coarbitrary a)) arbitrary);
  |}.

(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Instance shrinkFunNil {A B : Type} : Shrink (A -> B) :=
  {| shrink x := nil |}.

Section arbFun_completeness.

Variables A B : Type.
Hypothesis choice : FunctionalChoice_on A RandomSeed.

(* Goal: not (@eq nat m O) *)
(* begin arbFunCorrect *)
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
Theorem arbFunComplete `{CoArbitrary A, Arbitrary B} (max:A) (f:A-> B) (s:nat) :
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  s = Pos.to_nat (coarbitrary max) -> (semGenSize arbitrary s <--> setT) ->
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
  exists seed, forall a, coarbLe a max -> run arbitrary s seed a = f a.
(* Goal: not (@eq nat m O) *)
(* end arbFunCorrect *)
Proof.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
move=> eqsize semB.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
have/choice [fseed fseedP]: forall a, exists seed : RandomSeed, run arbitrary s seed = f a.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq RandomSeed (varySeed (posToPath (@coarbitrary A H a)) seed) (f a)) *)
  by move => a; case: (semB (f a))=> _ /(_ I) [seed ?]; exists seed.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
case: (coarbComplete max fseed) => seed Hseed.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
pose proof (randomSplitAssumption seed seed) as Hyp.
(* Goal: @ex RandomSeed (fun seed : RandomSeed => forall (a : A) (_ : @coarbLe A H a max), @eq B (@run (forall _ : A, B) (@arbitrary (forall _ : A, B) (@genFun A B H H0)) s seed a) (f a)) *)
move : Hyp => [seed' Hsplit].
(* Goal: and (lt m (S (S n))) (not (@eq nat m O)) *)
exists seed' => a le_a; rewrite -fseedP -Hseed //=.
apply (@promoteVariant A B a (fun a => posToPath (coarbitrary a)) arbitrary 
                       s seed' seed seed Hsplit).
Qed.

End arbFun_completeness.

