From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Program.Equality.

Require Import Arith_base.
Require Import Vectors.Fin.
Require Import Vectors.VectorDef.
Require Import Bool.

Class Lex (A : Set) (FCross : A -> A -> A) (CP : A -> A -> Prop) : Prop := {
    transformable : forall (x : A), {P | ~ CP x (P x)};
    anti_identity : forall (x y : A), ~ CP x y -> ~ CP x (FCross x y);
    convergent_equality : forall (x y : A), x = y -> CP x y;
    crossover_identity : forall (y : A), {x | ~ (CP x y) -> CP (FCross x y) y}
}.

Record P_Product {B A} {H : Set -> Set} (k : H A) C (perception : forall {x y : B} {k : H A}, C k x -> C k y -> Prop) : Type := P' {
  Px : B;
  Py : B;
  Px' : C k Px;
  Py' : C k Py;
  PE : perception Px' Py'
}.


Notation "f ∘ g" := (fun x => f (g x)) (at level 80, right associativity).

Section Env.
Variables X B A : Set.
Variable f : X -> X -> X.
Variable f' : X -> X -> bool.
Variable K : Lex f f'.
Variable H : Set -> Set.
Variable C : H A -> B -> Prop.
Variable point : forall x y , C x y -> A.

Class Agent (Lex' : Lex f f') (T : Set) := {
 memory : T -> X;
 perception : forall {x y : B} (k : H A), C k x -> C k y -> Prop;
 action : forall {x y : B} (k : H A) (x' : C k x) (y' : C k y), H A -> Prop;
}.

Variable AG : Agent K A.

Record Functions : Type := F' {
   faction : H A -> H A;
   flang : H A -> H A
}.


Record Interation k (P : Functions) : Prop := I' {
    consistency_action : forall (Pr : P_Product ((flang P) k) (@perception _ _ AG)),
                action (Px' Pr) (Py' Pr) ((faction P) ((flang P)k));

    knowlegde : forall (Pr : P_Product k (@perception _ _ AG)) (a : C ((flang P) k) (Px Pr)),
         memory (point a)  = (f (memory (point (Px' Pr))) (memory ((point (Py' Pr)))))

}.

Class Environment (k : H A) (H' : Functions) : Prop := {
  inhabited : forall (x : H A), {b | C x b};
  perceived : P_Product k (@perception _ _ AG);
  active : forall (k : H A), {y : (B * B) | {c : (C k (fst y) * C k (snd y)) | perception (fst c) (snd c)}};
  iterable : Interation k H';
}.

Class State {f' g'} {k} := {
  inductive_environment :
    Environment k (F' f' g') /\ (forall k (x :  Environment k (F' f' g')), Environment ((g' ∘ f') k) (F' f' g'));
}.


End Env.

Inductive binary := |zero : binary |one : binary.

Inductive lex n :=
|lex' : t binary (S n) -> lex n.

Fixpoint invert_binary {y} (x : t binary y) : t binary y.
induction x.
refine (nil _).
destruct h.
refine (cons _ one _ (invert_binary _ x)).
refine (cons _ zero _ (invert_binary _ x)).
Defined.

Theorem _not_conservation:
  forall n (x : lex n), {P : forall {n} {h : lex n}, lex n | x <> P n x}.
move => x'.
pose (fun y (x : lex y) =>
  match x with
    |@lex' _ v  => @lex' y (invert_binary v)
  end).
intros; exists l.
destruct x; simpl; injection; intros.
clear H.
move : H0.
elim/@caseS' : t.
intros.
destruct h.
inversion H0.
inversion H0.
Qed.


Export VectorNotations.

Definition case1 {A} (P : t A 1 -> Type)
  (H : forall h, @P [h]) (v: t A 1) : P v :=
match v with
  |h :: t => match t with
    |nil _ => H h
  end
  |_ => fun devil => False_ind (@IDProp) devil
end.

Definition case_2nat (P : nat -> nat -> Type)
  (H : P 0 0) (H' : forall y, P 0 (S y)) (H1 : forall x, P (S x) 0)
     (H2 : forall x y, P (S x) (S y))
   : forall x y, P x y.
move => x y.
destruct x.
destruct y.
exact H.
refine (H' y).
destruct y.
refine (H1 x).
refine (H2 x y).
Defined.

Definition case_2t {A} (P : forall n, t A (S n) -> t A (S n) -> Type)
    (H' : forall n a b (t t' : t A n), P _ (a :: t) (b :: t'))
   : forall n (x y : t A (S n)), P _ x y.
move => n x.
refine (match x in (t _ (S n)) return (forall (y : (t A (S n))), P n x y) with
  |@cons _ k q c => _
 end).
elim/@caseS'.
intros.
refine (H' _ k h _ _).
Defined.

Search (_ < _).

Definition rect_leb (A : Type) (P:forall {n} {y}, t A (S n) -> y < S n -> Type)
 (out_of_gas: forall a {n} (H : 0 < (S (S n))) (v: t A (S n)), P (cons _ a _ v) H)
 (min_length : forall a (H : 0 < 1) (v: t A 0), P (cons _ a _ v) H)
 (rect: forall a {n} {y} (H : S y < (S (S n))) (v: t A (S n)), P v (le_S_n _ _ H) -> P (cons _ a _ v) H) :
   forall {n} {y} (H : y < S n) (v: t A (S n)), P v H.
 refine (fix rectS_fix {n} {y} (H : y < S n) (v: t A (S n)) {struct v} : P _ _ v H :=
 (match v in t _ (S n) return (forall (H : y < S n),  P n _ v H) with
 |@cons _ a 0 v' =>
   (match v' in t _ 0 with
     |@nil _ => _
     |@cons _  _ l _ => _
   end)
 |@cons _ a (S nn') v1 => _
 |_ => fun devil => False_ind (@IDProp) devil
 end) _).

intros.
destruct y.
(*that's the fun case*)
refine (min_length a H0 (nil A)).
  have : ~ S _ < 1.
    case.
    move => // h.
    apply le_not_lt in h.
    assert (2 <= 2).
    auto with arith.
    tauto.
    cbv; intros.
    apply le_S_n in H1; apply le_not_lt in H1.
    assert(0 < S (S n1)).
    auto with arith.
    auto.
intros; destruct (x _ H0).
intros; destruct y.
exact idProp.
exact idProp.
intros.
destruct y.
refine (out_of_gas a _ H0 v1).
  have : y < S nn'.
  auto with arith.
move => H1.
refine (rect a _ _ H0 v1 (rectS_fix _ _ (le_S_n _ _ H0) v1)).
Defined.

Definition rect_2per {A} (P : forall n, t A (S n) -> Type)
  (H : forall n h a (t : t A (S n)), P _ (a :: t) -> P _ (h :: a :: t))
  (H1' : forall h v, @P 1 [h; v])
  (H0 : forall h, P 0 [h]):
     forall n (x : t A (S n)), P _ x.

  refine (fix fix_S n (v : t A (S n)) {struct v} : P n v := _).
  refine (match v as c in (t _ (S n)) return P n c with
  |cons _ h 0 v' => match v' with
      |@nil _ => _
    end
  | cons _ a (S (S n')) v' => _ (fix_S _ v')
  | cons _ a 1 v1 => _
  | _ => fun devil => False_rect (@IDProp) devil
  end).

elim/@case0 : v'; refine (H0 _).
elim/@caseS' : v1; intros.
elim/@case0 : t; refine (H1' _ _).
elim/@caseS' : v'; intros.
elim/@caseS' : v; intros.
refine (H _ a h _ x).
Defined.

(*
Inductive vec_ind {A} (P : forall n, t A (S n) -> Type)
   : forall {n} (v : t A (S n)), Type :=
  |bas : forall e, P 0 [e] -> vec_ind P [e]
  |bas2 : forall e h, P 1 [e;h] -> vec_ind P [e; h]
  |ind : forall n' (x : t A (S n')) e, vec_ind P x -> P _ (cons _ e _ x) -> @vec_ind A P (S n') (cons _ e _ x).


Definition v_ind {A n} (v : t A (S n)) P : vec_ind P v -> A.
elim.
refine (fun e H => e).
refine (fun e h H => e).
intros.
exact e.
Defined.

Definition rect_2per {A} (P : forall n, t A (S n) -> Type)
  (H : forall n h a (t : t A (S n)) (v : vec_ind P (h :: t)), P _ (a :: t) ->
  P _ (h :: (v_ind v) :: t))
  (H1' : forall h v, P _ [h;v])
  (H0 : forall h, P _ [h]):
     forall n (x : t A (S n)), vec_ind P x.

  refine (fix fix_S n (v : t A (S n)) {struct v} : vec_ind P v := _).
  refine (match v as c in (t _ (S n)) return vec_ind P c with
  |cons _ h 0 v' => match v' with
      |@nil _ => _
    end
  | cons _ a (S (S n')) v' => _ (fix_S _ v')
  | cons _ a 1 v1 => _
  | _ => fun devil => False_rect (@IDProp) devil
  end).


elim/@case0 : v'; refine (bas (H0 _)).
elim/@caseS' : v1; intros.
elim/@case0 : t.
refine (bas2 (H1' _ _)).
move => H3.
elim/@caseS' : v' H3; intros.
pose (H _ _ h _ H3).

refine (p a h _ x).
Defined.

*)


Definition rect_SS' {A} (P : forall n, t A (S n) -> Type)
  (H : forall n h a (t : t A (S n)), P _ t -> P _ (a :: h :: t)) (H' : forall h, @P 0 [h]) (H1' : forall h v, @P 1 [h; v]) : forall n (x : t A (S n)), P _ x.

  refine (fix fix_S n (v : t A (S n)) {struct v} : P n v := _).
  refine (match v as c in (t _ (S n)) return P n c with
  |cons _ h 0 v' => match v' with
      |@nil _ => _
    end
  | cons _ h 1 v1 => _
  | cons _ a (S (S n')) v' => _
  | _ => fun devil => False_rect (@IDProp) devil
  end).

intros.
refine (H' h).
intros.
refine (match v1 with
  |@cons _ k 0 q => match q in (t _ 0) with
    |@nil _ => _
  end
 end).

refine (H1' h k).
refine (match v' as c in (t _ (S (S n'))) return P (S (S n')) (a :: c) with
  |@cons _ k n q => _
 end).

destruct n.
exact idProp.
refine (H _ k a _ (fix_S _ q)).

Defined.


Definition rect_2S {A B} (P:forall {n}, t A (S n) -> t B (S n) -> Type)
  (bas : forall x y, P [x] [y]) (rect : forall {n} (v1 : t A (S n)) (v2 : t B (S n)), P v1 v2 ->
    forall a b, P (a :: v1) (b :: v2)) :
     forall {n} (v1 : t A (S n)) (v2 : t B (S n)), P v1 v2.

  refine (fix rect2_fix {n} (v1 : t A (S n)) : forall v2 : t B (S n), P _ v1 v2 :=
  match v1 in t _ (S n) with
  | [] => idProp
  | @cons _ h1 (S n') t1 => fun v2 =>
    caseS' v2 (fun v2' => P _ (h1::t1) v2') (fun h2 t2 => rect _ _ _ (rect2_fix t1 t2) h1 h2)
  |cons _ a 0 x' => fun (v2 : t B 1) => _
 end).

elim/@case0 : x'.
refine (match v2 with
  |cons _ b 0 y' => match y' with
      |nil _ => _
      |_ => _
    end
  end).

elim/@case0 : y'.
refine (bas a b).
exact idProp.
Defined.

Fixpoint cross_binary_vector {n} (x : t binary (S n)) (y : t binary (S n)) : t binary (S n).
elim/@rect_2S  : x/y.
intros.
refine (cons _ (match (x, y) with
  |(one, one) => one
  |(zero, zero) => zero
  |(x', y') => y'
 end) _ (nil _)) .
intros.
refine (match (a, b) with
  |(one, one) => (cons _ a _ (cross_binary_vector _ v1 v2))
  |(zero, zero) => (cons _ a _ (cross_binary_vector _ v1 v2))
  |(x', y') => (cons _ b _ v1)
 end).

Defined.


Definition cross_lex {n} (x : lex n) (y : lex n) : lex n.
constructor.
destruct x.
destruct y.
refine (cross_binary_vector t t0).
Defined.


Definition b_rect (P : binary -> binary -> Type) (H : P one one) (H' : P zero zero) (H1' : P one zero) (H2' : P zero one) (x y : binary) : P x y.
intros.
destruct x.
destruct y.
move => //=.
move => //=.
destruct y.
move => //=.
move => //=.
Defined.

Theorem crossover_binary :
  forall   n
           (x : t binary (S n))
           (y : t binary (S n)),
           x <> y ->
           x <> cross_binary_vector x y.

  have : forall t t0, lex' t <> lex' t0 -> t <> t0.
  intros.
  cbv in H.
  cbv.
  move => h'.
    have : lex' t = lex' t0.
    congruence.
  tauto.

  have : forall n h x y, cons _ n h x <> cons _ n h y -> x <> y.
   intros.
   move => H'.
   congruence.
  move => H'.

  have : forall h n x y, x <> y -> cons _ n h x <> cons _ n h y.
   intros.
   move => H2'.
   pose (fun a n (x : t a (S n)) => match x in (t _ (S n)) with
     |@cons _ _ _ x => x
     end).
   pose (@f_equal (t T (S h)) (t T h) (@y0 _ _) _ _ H2').
   simpl in e.
   tauto.
 move => K.

intros.
move : H; elim/@rect_2S : y/x0.
intros; unfold cross_binary_vector; simpl in *.
by move : H; elim/@b_rect : x0/y.
intros; move : H0 H; elim/@b_rect : a/b.
intros.
unfold cross_binary_vector; simpl; fold @cross_binary_vector.
apply H' in H0; apply H in H0.
auto.
intros.
unfold cross_binary_vector; simpl; fold @cross_binary_vector.
apply H' in H0; apply H in H0;apply : K.
trivial.
intros.
unfold cross_binary_vector; simpl; fold @cross_binary_vector.
move => H2'.
inversion H2'.
intros.
unfold cross_binary_vector; simpl; fold @cross_binary_vector.
move => H2';inversion H2'.
Qed.

Definition eq_vector_binary : forall (n : nat), t binary n -> t binary n -> bool.
  pose (fun (x y : binary) => match (x, y) with
  |(one, one) => true
  |(zero, zero) => true
  |(x, y) => false
  end).

  refine (fix fix_S n (t t0 : t binary n) {struct t} := _).
  elim/@rect2 : t/t0.
  refine (true).
  intros;refine ((b a b0) && (fix_S _ v1 v2)).
Defined.

Definition lex_binary : forall (n : nat), lex n -> lex n -> bool.
intros.
destruct H.
destruct H0.
refine (eq_vector_binary t t0).
Defined.

Theorem lex_vec_eq : forall n (v y : t binary (S n)), eq_vector_binary v y = true -> v = y.
intros.
move : H.
elim/@rect_2S : v/y.
move => x y.
elim/b_rect : x/y.
trivial.
trivial.
simpl in *; congruence.
simpl in *; congruence.
intros.
move : H0.
elim/b_rect : a/b.
 - intros; simpl in *; apply H in H0; congruence.
 - intros; simpl in *; apply H in H0; congruence.
 - intros; simpl in *; congruence.
 - intros; simpl in *; congruence.
Qed.

Theorem lex_eq : forall n (v y : lex n), lex_binary v y = true -> v = y.
intros.
destruct v. destruct y.
unfold lex_binary in H.
pose (lex_vec_eq H).
congruence.
Qed.

Definition lex_prop : forall (n : nat), lex n -> lex n -> Prop.
intros.
exact (lex_binary H H0 = true).
Defined.

Fixpoint imperfect_binary_cpy {n} (x : t binary (S n)) : t binary (S n).
elim/@rectS : x.
case.
exact (cons _ one _ (nil _)).
exact (cons _ zero _ (nil _)).
intros.
refine (cons _ a _ (imperfect_binary_cpy _ v)).
Defined.

Theorem unique_binary_object_convergent_complement {n} (y : t binary (S n)) :
   {x | x <> y -> cross_binary_vector x y = y}.
exists (imperfect_binary_cpy y).
move : y; elim/@rectS.
case => //=.
case => //= H' V hi h.
have : imperfect_binary_cpy V <> V.
congruence.
move => H.
have : cross_binary_vector (imperfect_binary_cpy V) V = V.
apply : hi H; move => H3.
congruence.
have : imperfect_binary_cpy V <> V.
congruence.
move => H.
have : cross_binary_vector (imperfect_binary_cpy V) V = V.
apply : hi H; move => H3.
congruence.
Qed.

Theorem lex_binary_eqv : forall {n} (m : lex n), lex_binary m m = true.
  intros.
  destruct m.
  elim/@rectS : t.
  by destruct a.
  by elim.
Qed.


Theorem neg_of_convergent_lex : forall n (x : lex n) y, x <> y -> lex_binary x y = false.

  have : forall x y, lex_binary x y = false -> ~ lex_binary x y = true.
  move => n0 x0 y0.
  destruct (lex_binary x0 y0).
  move => h2.
  inversion h2.
  move => H2 H3.
  inversion H3.

intros.
destruct x0.
destruct y.
move : H.
elim/@rect_2S : t/t0.
move => x0 y.
elim/@b_rect : x0/y.
intros.
destruct H.
auto.
intros.
destruct H.
auto.
auto.
intros.
done.
intros.
move : H H0.
pose (fun n (x : t binary (S n)) => match x in t _ (S n) with
  |a :: b => b
 end).
pose (fun n (x : t binary (S n)) => match x in t _ (S n) with
  |a :: b => a
 end).
  have : forall x v v', lex' (x :: v) <> lex' (x :: v') -> lex' v <> lex' v'.
  case => n1. elim/@caseS'.
  move => h n2; elim/@caseS'.
  move => h0; elim/@case0.
  elim/@case0 : n2.
  intros; move => H2.
  injection H2; move => n2; subst.
  by contradiction H.
  intros.
  move => H2'.
     have : v = v'.
     congruence.
  move => H3; rewrite H3 in H.
  by contradiction H.
move => H2'.
elim/@b_rect : a/b.
intros; simpl in *; apply H2' in H0.
tauto.
intros; apply H2' in H0; tauto.
intros; trivial.
intros; trivial.
Qed.

Theorem neg_of_convergent_lex' : forall n (x : lex n) y, lex_binary x y = false -> x <> y.

  have : forall x y, lex_binary x y = false -> ~ lex_binary x y = true.
  move => n0 x0 y0.
  destruct (lex_binary x0 y0).
  move => h2.
  inversion h2.
  move => H2 H3.
  inversion H3.

intros.
apply x in H.
move => H2.
destruct x0.
destruct y.
move : H2 H.
elim/@rect_2S : t/t0.
move => x0 y.
elim/@b_rect : x0/y.
auto.
auto.
intros; inversion H2.
intros; inversion H2.
move => n0 v1 v2 H a b.

pose (fun n (x : t binary (S n)) => match x in t _ (S n) with
  |a :: b => b
 end).

elim/@b_rect : a/b.
intros.
simpl in *.
  have : one :: v1 = one :: v2.
  congruence.
move => e'.
apply (@f_equal _ _ (@y (S n0))) in e'; simpl in e'.
  have : lex' v1 = lex' v2.
  congruence.
auto.
intros.
simpl in *.
  have : zero :: v1 = zero :: v2.
  congruence.
move => e'.
apply (@f_equal _ _ (@y (S n0))) in e'; simpl in e'.
  have : lex' v1 = lex' v2.
  congruence.
auto.
intros.
inversion H2.
intros.
inversion H2.
Qed.


Fixpoint pow_f' {A} (x : nat) (f : A -> A) {struct x} : x > 0 -> (A -> A).
  refine (match x with
    |(S x') => (fun x' => match x' as c return c = x' -> S c > 0 -> A -> A with
                 |S y => _
                 |0 => _
               end) x' eq_refl
    |0 => fun H => match ((gt_irrefl 0) H) with end
  end).
refine (fun e h => f).
intros.
  have : S y > 0.
  auto with arith.
move => H2.
rewrite H in H2.
move : X.
refine ((pow_f' _ _ f H2) ∘ f).
Defined.

Fixpoint pow_f {A} (f : A -> A) (x : nat) {struct x} : A -> A :=
  match x with
    |(S x') => f ∘ (pow_f f x')
    |0 => f
  end.

Fixpoint pow_tf {A} (f : A -> A) (y : A) (x : nat) {struct x} : A :=
  match x with
    |(S x') => f (pow_f f x' y)
    |0 => f y
  end.

Theorem fpow_eq_cons : forall n1 l g (v3 v0 : t binary (S n1)), g
     :: cross_binary_vector
          (pow_f (cross_binary_vector^~ v3) l v0) v3 =
     cross_binary_vector
       (pow_f (cross_binary_vector^~ (g :: v3)) l (g :: v0))
       (g :: v3).

intros.
induction l.
simpl in *.
by destruct g.

move : IHl.
elim/@rect_2S : v3/v0.
Ltac finish_feqv g IHl := intros; destruct g; simpl; by rewrite <- IHl.
by finish_feqv g IHl.
by finish_feqv g IHl.
Qed.

Theorem fpow_eq_cons' : forall n1 l g w (v3 v0 : t binary (S n1)), w <> g ->
          g :: (pow_f (cross_binary_vector^~ v3) l v0) =
                  (pow_f (cross_binary_vector^~ (g :: v3)) (S l) (w :: v0)).


intros.
move : H.
induction l.
elim/@b_rect : w/g.
congruence.
congruence.
trivial.
trivial.
intros.
apply IHl in H; clear IHl; simpl in *.
rewrite <- H; simpl in *.
by destruct g.
Qed.

Theorem cross_eq : forall n (v2 : t binary (S n)), (cross_binary_vector v2 v2) = v2.
move => n; elim/@rectS.
by destruct a.
intros.
destruct a.
simpl; by rewrite H.
simpl; by rewrite H.
Qed.

Theorem convergent_pair_totally : forall {n} (x y : t binary (S n)), eq_vector_binary ((pow_f (fun x => cross_binary_vector x y) (S n)) x) y = true.
  intros.
  elim/@rect_2S : x/y.
  intros.
  by elim/@b_rect : x/y.
  move => n0 v1 v2.
  intros.
  simpl in *.
      have : one <> zero.
    congruence.
  move => pH.
  elim/@b_rect : a/b.
  Ltac solve_powf_cross v1 v2 H :=
     rewrite <- (fpow_eq_cons _ _ v1 v2);
     simpl;
     rewrite  (lex_vec_eq H);
     rewrite (cross_eq _);
     set f := (@lex_binary_eqv _ (lex' v1)).

 Ltac solve_powf_cross' n0 v1 v2 H v v' proof_inv' :=
    change
     (cross_binary_vector
        (pow_f (cross_binary_vector^~ (_ :: v2)) _ (_ :: v1))
        (_ :: v2)) with
       (pow_f (cross_binary_vector^~ (v' :: v2))
   (S n0) (v :: v1));
  rewrite <- (fpow_eq_cons' _ v2 v1 proof_inv');
  simpl;
  rewrite <- H.

  by solve_powf_cross v2 v1 H.
  by solve_powf_cross v2 v1 H.
  by solve_powf_cross' n0 v1 v2 H one zero pH.
  by solve_powf_cross' n0 v1 v2 H zero one (not_eq_sym pH).
Qed.

Definition pure_lex l n := t (t binary (S l)) (S n).

Instance binary_lex : forall x, Lex (@cross_lex x) (@lex_prop x).
 {

  constructor.

  (* The proof of lex transform *)
  intros.
  pose (_not_conservation x0).
  destruct s.
  exists (x1 x).
  apply not_true_iff_false.
  apply (neg_of_convergent_lex).
  trivial.

  (*Anti-identity proof of crossover function *)
  intros.
  destruct x0.
  destruct y.
  unfold lex_prop in *.
  apply not_true_iff_false.

  apply not_true_is_false in H.
  apply neg_of_convergent_lex.
  apply neg_of_convergent_lex' in H.
  move => H2.
  unfold cross_lex in H2.
    have : t <> t0.
    congruence.
  move => H2'.
  pose (@crossover_binary _ _ _ H2').
  congruence.

  (*Convergence implies to definitional equality *)
  intros.
  unfold lex_prop.
  rewrite H.
  clear H x0.
  apply : lex_binary_eqv.

  (*Existence of Convergence aproximation from x to y*)
  intros.
  destruct y.
  destruct (unique_binary_object_convergent_complement t).
  exists (lex' x0).
  move => H'.
  unfold lex_prop in *.

  apply not_true_is_false  in H'.
    have : x0 <> t.
    set (neg_of_convergent_lex' H'); congruence.
  move => H.
  apply e in H.
  unfold cross_lex.
  rewrite H.
  apply : lex_binary_eqv.
}
Defined.

Inductive SAgent n :=
   T' : lex n -> SAgent n.

Definition agent_lex {n} (x : SAgent n) :=
  match x with
    |@T' _ l => l
 end.

Fixpoint len {a} {n} (x : t a n) :=
  match x with
    |_ :: y => (len y) + 1
    |[] => 0
  end.


(*The class Agent is just a proof that there is a depedent product of a lex
  and one construction and the depedent product carry a memory that map the construction
   with one lexical memory *)

Definition get_agent {n} {l} (ls : t (SAgent n) l) (y : nat) (H : y < l) : SAgent n := nth_order ls H.

Definition boundness {n} {l} (ls : t (SAgent n) l) (y : nat) : Prop := y < l.

Definition view {l} {n} {y} {y'} (v : t (SAgent n) (S l)) (H : y < (S l)) (H' : y' < (S l)) :=
  (y =? 0) && (y' =? l) = true.

Definition action_prop {l} {n} {y} {y'} (v : t (SAgent n) (S l)) (H : y < S l) (H' : y' < S l) : t (SAgent n) (S l) -> Prop.
move => v'.
refine (get_agent v H = get_agent v' H').
Defined.

Definition match_lex {l} {n} (v : t (SAgent n) (S l)) : t (SAgent n) (S l).

  have : 0 < S l /\ l < S l.
  auto with arith.
move => h.
destruct h.
set f' := v[@of_nat_lt H].
set s' := v[@of_nat_lt H0].

exact (replace (replace v (of_nat_lt H0) (T' (cross_lex (agent_lex s') (agent_lex f'))))
  (of_nat_lt H) (T' (cross_lex (agent_lex f') (agent_lex s')))).

Defined.

Instance SAgent' : forall x y, @Agent _ _ _ _ _ (
  fun x => t x (S y)) (@boundness x  _) (binary_lex x) (SAgent x). {
  constructor.
  refine (@agent_lex x).
  move => x0 y0.
  exact view.
  move => x0 y0.
  exact action_prop.
}
Defined.


Definition tail := (fun a n (v : t a (S n))  => match v in (t _ (S n)) with
   |@cons _ _ _ v' => v'
   |@nil _ => idProp
 end).

Theorem head_get : forall a n (x : t a (S n)) (H : 0 < (S n)), hd x = nth x (Fin.of_nat_lt H).
intros.
move : H.
by elim/@caseS : x.
Qed.

Theorem last_tail : forall a n (x : t a (S n)) (H : n < (S n)), last x = nth x (Fin.of_nat_lt H).
intros.
move : H.
elim/@rectS : x.
intros.
by simpl.
intros.
simpl in *.
generalize (lt_S_n n0 (S n0) H0).
move => t.
pose (H t).
trivial.
Qed.

Theorem shift_hd_get' : forall A n (x : t A (S n)) (H : n < (S n)) (a : A), (shiftin a x)[@FS (Fin.of_nat_lt H)] = a.
intros.
move : H.
elim/@rect_SS' : x.
intros.
simpl in *.
by set (H (lt_S_n n0 (S n0)
                       (lt_S_n (S n0)
                          (S (S n0)) H0))).
trivial.
intros.
simpl in *.
trivial.
Defined.

Theorem of_nat_lt_c : forall x y (v : x < y) (v' : x < y), of_nat_lt v = of_nat_lt v'.
move => x y.
elim/@nat_double_ind : x/y.
intros.
destruct n.
inversion v.
simpl in *; trivial.
intros;inversion v.
intros.
set (H (lt_S_n n m v) (lt_S_n n m v')); simpl in *; rewrite e.
reflexivity.
Qed.

Definition shift {l} {n} (v : t (SAgent n) (S l)) : t (SAgent n) (S l).
destruct l.
exact v.
destruct l.
refine (cons _ (hd (tail v)) _ (cons _ (hd v) _ (nil _))).
refine (shiftin (hd v) (tail v)).
Defined.


Theorem inj : forall n l (x y : t (SAgent n) (S l)), shift x = shift y -> x = y.
  have : forall a b v1 v2, shiftin a v1 = shiftin b v2 -> v1 = v2 /\ a = b.
  intros.
  move : H.
  elim/@rect2 : v1/v2.
  constructor; trivial.
  simpl in H; congruence.
  intros.
  simpl in *.
  pose (fun n (x : t T (S n)) => match x in (t _ (S n)) with
     |@cons _ _ _ y => y
   end).
  pose (fun n (x : t T (S n)) => match x in (t _ (S n)) with
     |@cons _ x _ _ => x
   end).
 set (f_equal (@y0 _) H0).
 set (f_equal (@y _) H0).
 simpl in *.
 apply H in e0.
 destruct e0.
 constructor.
 congruence.
 trivial.

intros; move : H.
elim/@rect_2S : x0/y.
trivial.
intros.
destruct n0.
simpl in H0; injection H0; move : H H0.
elim/@caseS' : v1; elim/@caseS' : v2.
move => h t h0 t0.
elim/@case0 : t; elim/@case0 : t0.
intros.
simpl in *; subst; trivial.
simpl in *.
destruct n0.
by destruct (@x _ _ a b _ _ H0); subst.
by destruct (@x _ _ a b _ _ H0); subst.
Qed.

Theorem shift_back : forall n s (x : t (SAgent s) (S n)) (H : n < S n) (H' : 0 < S n), (shift x)[@of_nat_lt H] = x[@of_nat_lt H'].
move => n s.
elim/@rect_SS'.
intros;simpl in *; apply : shift_hd_get'.
done.
done.
Qed.

Theorem law1 : forall l y (k : t (SAgent l) (S y)) (x' : y < S y) (y' : 0 < S y), get_agent (match_lex k) y' = get_agent (shift (match_lex k)) x'.
  intros.
  move : x' y'.
  unfold get_agent.
  unfold nth_order.
  elim/@rectS : k.
  done.
  destruct n.
  done.
  simpl; unfold caseS'.
  elim/@caseS'.
  intros;move : H; elim/@caseS' : t.
  intros;symmetry.
  apply : shift_hd_get'.
Qed.

Theorem law2 : forall  l y (k : t (SAgent l) (S y)) (x' : y < S y) (y' : 0 < S y), agent_lex (match_lex k)[@of_nat_lt y'] = cross_lex (agent_lex k[@of_nat_lt y']) (agent_lex k[@of_nat_lt x']).
  move => l y.
  elim/@rectS.
  intros; trivial.
  intros; simpl in *.
  by rewrite (of_nat_lt_c (lt_S_n n (S n) (le_n (S (S n)))) (lt_S_n n (S n) x')).
Qed.

Definition binary_crossing {l n} (x : pure_lex l n) : pure_lex l n :=
  shiftin (cross_binary_vector (hd x) (last x)) (tl x) .

Fixpoint binary_crossing' {l n} (x : pure_lex l n) {struct x} : pure_lex l n.
  elim/@rectS : x.
  intros.
  refine (cons _ a _ (nil _)).
  intros.
  refine (_ (binary_crossing' _ _ v)).
  move => K.
  elim/@caseS' : K.
  intros.
  refine (cons _ (cross_binary_vector a h) _ (h :: t)).
  Show Proof.
Defined.

Require Import FunInd.

Fixpoint cut_binary {l n} (x : pure_lex (S l) n) : pure_lex l n.
elim/@rectS : x.
refine (fun a => cons _ (take _ (le_S _ _(le_n (S l))) a) _ (nil _)).
intros.
refine (cons _ (take _ (le_S _ _(le_n (S l))) a) _ (cut_binary _ _ v)).
Defined.

Definition whole_crossing {l n} (x : pure_lex l n) : pure_lex l n :=
  pow_f binary_crossing (S l) (pow_f binary_crossing (S n) x).

Definition equal_binary (x y : binary) : bool := match (x, y) with
   |(one, one) => true
   |(zero, zero) => true
   |(_, _) => false
 end.

Fixpoint eq_vec_partial_eqv {l} (x : t binary (S l)) (y : t binary (S l)) n (H : n < S l) : Prop.
intros;elim/@rect_leb : x/H y.
intros;elim/@caseS' : y.
intros.
refine (equal_binary a h = true).
intros; elim/@caseS' : y.
intros. refine (equal_binary a h = true).
intros; elim/@caseS' : y0.
intros.
refine ((equal_binary a h = true) /\ eq_vec_partial_eqv _ v t _ (le_S_n _ _ H)).
Defined.

Fixpoint eq_vec_binary_quantification {l} (x : t binary (S l)) (y : t binary (S l)) : nat -> nat.
elim/@rect_2S : x/y.
refine (fun x y n => match (x, y) with
    |(one, one) => n + 1
    |(zero, zero) => n + 1
    |(_, _) => n
  end).
intros.
refine (match (a, b) with
    |(one, one) => eq_vec_binary_quantification _ v1 v2 H0 + 1
    |(zero, zero) => eq_vec_binary_quantification _ v1 v2 H0 + 1
    |(_, _) => H0
  end).
Defined.

Definition eqv_progress {n y} (b : binary) (H : y < S n) (v : t binary (S n)) : Prop.
intros.
refine (nth v (of_nat_lt H) = b).
Defined.

Fixpoint count_progress {n} (v v' : t binary (S n)) (y' : nat) {struct v} : nat.
intros.
pose (fun x y (f : nat) f' => match (x, y) with
                        |(one, one) => f
                        |(zero, zero) => f
                        |(_, _) => f'
         end).

elim/@rect_2S : v/v'.
intros.
refine (n0 x y (y' + 1) y').
intros.
refine ((n0 a b ((count_progress _ v1 v2 y') + 1) (count_progress _ v1 v2 y'))).
Show Proof.
Defined.

Theorem count_sym : forall n (v1 v2 : t binary (S n)),
  (count_progress v2 v1 0) = (count_progress v1 v2 0).

intros.
elim/@rect_2S : v1/v2.
intros; by elim/@b_rect : x/y.
intros.
elim/@b_rect : a/b.
simpl in *; auto.
simpl in *; auto.
simpl in *; auto.
simpl in *; auto.
Qed.

Theorem despesero : forall {n} (x y : t binary (S n)), last x <> last y ->
  count_progress y (cross_binary_vector x y) 0 =
        S (count_progress x y 0).
 intros.
 move : H.
 elim/@rect_2S : x/y.
 intros.
 move : H.
 by elim/@b_rect : x/y.
 intros.
 move : H0.
 elim/@b_rect : a/b.
 intros; simpl in *; apply H in H0; by rewrite H0.
 intros;simpl in *; apply H in H0; by rewrite H0.
 intros; apply H in H0; simpl in *; rewrite <- (plus_n_Sm _ _); rewrite <- (plus_n_O _); by rewrite <- (count_sym _ _).
 intros; apply H in H0; simpl in *; rewrite <- (plus_n_Sm _ _); rewrite <- (plus_n_O _); by rewrite <- (count_sym _ _).
Qed.

Theorem shift_hd : forall {A n} (x : t A (S n)) h,
  hd (shiftin h x) = (hd x).
 intros.
 induction n.
 elim/@caseS' : x.
 move => h0.
 by elim/@case0.
 by elim/@caseS' : x.
Qed.

Fixpoint prop_list {A n}
   (v : t A (S n)) (P : A -> A -> Prop) {struct v} : Prop.
intros.
elim/@rectS: v.
intros.
refine (P a a).
intros.
clear X.
refine (_ (prop_list _ _ v P)).
move => K.
elim/@caseS' : v.
move => a' v'.
exact (P a a' /\ K).
Defined.

Fixpoint to_back {A n} (x : t A n) (y : A) {struct x} : t A n.
destruct n.
refine (nil _).
elim/@rectS : x.
intros;refine (cons _ y _ (nil _)).
intros;refine (cons _ a _ (to_back _ _ v y)).
Defined.

Theorem one_le : forall n, 1 < (S (S n)).
 auto with arith.
Qed.

Theorem hd_get' : forall {A n} (x : t A (S n)), hd x = x [@F1].
 intros.
 by elim/@rectS : x.
Qed.

Theorem sym_binary_pair : forall n q (x y : t binary (S n)) (H : q < S n) b,
   x[@of_nat_lt H] = b -> y [@of_nat_lt H] = b ->
         (cross_binary_vector x y) [@of_nat_lt H] = b.
  intros.
  move : H x y H0 H1.
  elim/@nat_double_ind : n/q.
  intros; simpl in *; move : H0 H1.
  elim/@caseS' : x; elim/@caseS' : y.
  intros; move : H0 H1.
  by elim/@case0 : t; elim/@case0 : t0; elim/@b_rect : h/h0.
  intros; move : H0; elim/@caseS' : x.
  move : H1; elim/@caseS' : y.
  intros; simpl in *; move : H1 H0.
  by elim/@b_rect : h/h0.
  intros; simpl in *; move : y H0 H1 H2; elim/@caseS' : x.
  intros; move : t H0 H1 H2 H; elim/@caseS' : y.
  intros; simpl in H1; simpl in H2.
  pose (H (lt_S_n m (S n) H0) _ _ H1 H2).
  simpl in *.
  by elim/@b_rect : h/h0.
Qed.

Theorem vec_cons : forall A n (x : t A (S n)), x = x[@F1] :: (tl x).
  intros.
  by elim/@rectS : x.
Qed.

Theorem hd_bin : forall n m (x : t (t binary (S m)) (S (S n))),
    (binary_crossing' x)[@F1] = cross_binary_vector x[@F1]
    (binary_crossing' x)[@FS F1].
  intros.
  elim/@caseS' : x.
  intros.
  simpl.
  by rewrite (vec_cons (binary_crossing' _)).
Qed.

Theorem cons_bin : forall {n m} (x : t (t binary (S m)) (S (S n))),
   binary_crossing' x = cross_binary_vector x[@F1] (binary_crossing' x)[@FS F1]
                       :: (tl (binary_crossing' x)).

  intros.
  elim/@caseS' : x.
  intros.
  simpl.
  by rewrite (vec_cons (binary_crossing' _)).
Qed.

Hint Rewrite hd_bin : cross.

Theorem tl_bin : forall n m (x : t (t binary (S m)) (S (S n))),
   tl (binary_crossing' x) = (binary_crossing' (tl x)).
 Ltac case3S' x := elim/@caseS' : x; move => h3 x; elim/@caseS' : x; move => h3' x; elim/@caseS' : x.
 Ltac case2' x := elim/@caseS' : x; move => h3 x; elim/@caseS' : x; move => h3' x.
 intros.
 induction n.
 by case2' x; elim/@case0 : x.
 intros.
 elim/@caseS' : x.
 intros.
 simpl.
 by rewrite (cons_bin).
Qed.

Hint Rewrite tl_bin : cross.

Theorem cross_eq_pair_sym : forall n i (x y : t binary (S n)) a (H : i < S n),
    (cross_binary_vector x y) [@of_nat_lt H] = a -> y [@of_nat_lt H] = a \/ x [@of_nat_lt H] = a.
  move => i n.
  elim/@nat_double_ind : i/n.
  intros;move : H0.
  elim/@caseS' : x; elim/@caseS' : y.
  intros;move : H0.
  elim/@case0 : t; elim/@case0 : t0.
  intros;move : H0;left;move : H0.
  by elim/@b_rect : h0/h.
  intros.
  simpl in *;move : y H H0;elim/@rectS : x.
  intros;move : H0.
  elim/@caseS' : y; intros; move : H0; elim/@case0 : t.
  simpl; elim/@b_rect : a0/h.
  destruct a.
  move => H3; inversion H3.
  intros; by left.
  destruct a.
  by right.
  intros; by left.
  destruct a.
  intros; auto.
  intros; auto.
  destruct a.
  intros; auto.
  intros; auto.
  intros; simpl in *;move : H1; elim/@caseS' : y.
  intros; simpl in *.
  destruct a.
  move : H1; elim/@b_rect : a0/h; intros; simpl in *.
  intros; auto.
  intros; auto.
  intros; auto.
  intros; auto.
  move : H1; elim/@b_rect : a0/h.
  intros; auto.
  intros; auto.
  intros; auto.
  intros; auto.
  intros; simpl in *; move : H1.
  elim/@caseS' : x; elim/@caseS' : y.
  intros; simpl in *.
  pose (H t0 t a (lt_S_n m (S n) H0)).
  move : H1; elim/@b_rect : h/h0.
  simpl in *; auto.
  simpl in *; auto.
  simpl; intros; auto.
  simpl; intros; auto.
Qed.

Hint Rewrite cross_eq_pair_sym : cross.


Fixpoint pow_' {A} (f : A -> A) (x : nat) {struct x} : A -> A :=
  match x with
    |(S x') => f ∘ (pow_' f x')
    |0 => id
  end.

Theorem tl_pow_f_bin : forall n m q (v : t (t binary (S m)) (S n)) h,
  tl (pow_' binary_crossing' q (h :: v))
   = (pow_' binary_crossing' q v).
 intros.
 move : v h.
 induction q.
 intros.
 by elim/@rect_2per : v.
 intros; elim/@rect_2per : v IHq.
 intros.
 pose (IHq (h0 :: a :: t) h).
 by  rewrite (tl_bin _); fold @pow_'; rewrite e;simpl.
 by intros; simpl; rewrite (tl_bin _); rewrite (IHq [h0;v] h).
 intros; simpl.
 pose (IHq [h] h0).
 destruct q.
 trivial.
 by simpl in *; rewrite (tl_bin _); rewrite (IHq _ h).
Qed.

Hint Rewrite tl_pow_f_bin : cross.

Hint Rewrite vec_cons : cross.

(*
Theorem cons_powtf : forall m n0 h q (v : VectorDef.t (t binary (S m)) (S n0)) (H : q <= S n0),

(pow_' binary_crossing' (S q) (h :: v)) =
      cross_binary_vector (nth (pow_' binary_crossing' q (h :: v)) (of_nat_lt (Nat.lt_0_succ _)))
                          (nth (pow_' binary_crossing' q (h :: v)) (of_nat_lt (one_le _)))
           :: (pow_' binary_crossing' (S q) v).
    intros.
    move : H.
    elim/@caseS : v.
    intros.
      have :
  hd (pow_' binary_crossing' (S q) (h :: h0 :: t)) = cross_binary_vector
  (pow_' binary_crossing' q (h :: h0 :: t))[@
  of_nat_lt (Nat.lt_0_succ _)]
  (pow_' binary_crossing' q ((h :: h0 :: t)))[@
  of_nat_lt (one_le _)].
  intros.
  rewrite (hd_get').
  rewrite (hd_bin _ ).
   intros.
   fold @pow_'.
   simpl.
   by rewrite (of_nat_lt_c  (one_le n)).

   auto with arith.

  move => hd'.
    have : (tl (pow_' binary_crossing' (S q) (h :: h0 :: t)))
  =  pow_' binary_crossing' (S q) (h0 :: t).

    rewrite(tl_bin _).
    fold @pow_'.
    by rewrite (tl_pow_f_bin _).

    move => H3.
    simpl in *.
    rewrite <- hd'.
    rewrite <- H3.
    apply : vec_cons.
Qed.


Theorem binary_S : forall b n0 c (v : t (t _ (S b)) (S n0)),
  binary_crossing' (pow_' binary_crossing' c v) =
      (pow_' binary_crossing' (S c) v).
intros.
trivial.
Qed.

Theorem cons_powtf' : forall m n0 h c q (v : VectorDef.t (t binary (S m)) (S n0)) (H : q <= S n0),

(pow_' binary_crossing' (S q) (c :: h :: v)) =
      cross_binary_vector (nth (pow_' binary_crossing' q (c :: h :: v)) (of_nat_lt (Nat.lt_0_succ _)))
                          (nth (pow_' binary_crossing' q (c :: h :: v)) (of_nat_lt (one_le _)))
      ::
             cross_binary_vector (nth (pow_' binary_crossing' q (h :: v)) (of_nat_lt (Nat.lt_0_succ _)))
                          (nth (pow_' binary_crossing' q (h :: v)) (of_nat_lt (one_le _)))

      :: (pow_' binary_crossing' (S q) v).
   intros.
   elim/@caseS' : v.
   intros.
     have : hd (pow_' binary_crossing' (S q) (c :: h :: h0 :: t)) =
                cross_binary_vector
  (pow_' binary_crossing' q (c :: h :: h0 :: t))[@
  of_nat_lt (Nat.lt_0_succ (S (S n0)))]
  (pow_' binary_crossing' q (c :: h :: h0 :: t))[@
  of_nat_lt (one_le (S n0))].

    rewrite (hd_bin _ _).
    fold @pow_'; trivial.
    auto with arith.
   move => hd'.
      have : tl (pow_' binary_crossing' (S q) (c :: h :: h0 :: t) ) =
               cross_binary_vector
     (pow_' binary_crossing' q (h :: h0 :: t))[@of_nat_lt
                                                 (Nat.lt_0_succ (S n0))]
     (pow_' binary_crossing' q (h :: h0 :: t))[@of_nat_lt (one_le n0)]
   :: pow_' binary_crossing' (S q) (h0 :: t).

       rewrite(tl_bin _).
    rewrite (tl_pow_f_bin _).
    apply : cons_powtf.
    assumption.
    move => tl';rewrite <- hd';rewrite <- tl';apply : vec_cons.
Qed.

Hint Rewrite cons_powtf : cross.
Hint Rewrite cons_powtf' : cross.
*)

Fixpoint pred_binary_set {n m} (v : t (t binary (S m)) (S n)) :
  t (t binary m) (S n).
  intros; elim/@rectS : v.
  intros; refine (cons _ (tl a) _ (nil _)).
  intros; refine (cons _ (tl a) _ (pred_binary_set _ _ v)).
  Defined.

Theorem rewrite_prop_list : forall {A} {n} (x : t A (S n)) (P : A -> A -> Prop) (F : A -> A -> Prop),
   prop_list x P -> (forall x y, P x y -> F x y) -> prop_list x F.
  intros.
  elim/@rect_2per : x H.
  intros; destruct H1; pose (H H2).
  constructor.
  by apply : H0.
  by exact p.
  intros;by simpl in *; apply : H0.
  intros;by simpl in *; apply : H0.
Qed.

Theorem nth_prop_list : forall {A} {n} y (x : t A (S n)) (P : A -> A -> Prop) (H : y < S n) (H' : S y < S n),
     prop_list x P -> P (nth x (of_nat_lt H)) (nth x (of_nat_lt H')).
  intros;elim/@rect_leb : x/H H0 H'.
  intros; elim/@rect_2per : v H H' H0.
  by intros; simpl in *; destruct H1.
  simpl; tauto.
  simpl; tauto.
  intros; inversion H'; inversion H2.
  intros.
    have : S y0 < S n0.
    auto with arith.
  move => H3; elim/@caseS' : v H0 H1 H3.
  intros; destruct n0; simpl in H1.
  inversion H3; inversion H4.
  destruct n0; simpl in H1.
  elim/@caseS' : t H0 H1 H3.
  intros;elim/@case0 : t H0 H1.
  intros; destruct H1; pose (H0 H2 H3).
  simpl in p; simpl.
  rewrite <- (of_nat_lt_c (le_S_n (S y0) 2 H) ).
  by rewrite <- (of_nat_lt_c (lt_S_n y0 1 H3)).
  destruct H1.
  pose (H0 H2 H3).
  simpl in p; simpl.
  rewrite <- (of_nat_lt_c (le_S_n _ _  H)).
  by rewrite <- (of_nat_lt_c (lt_S_n _ _ H3)).
Qed.

(*
Theorem progress_pred : forall {q l a n} (v : pure_lex l n) (H : q < S l)
    (y : t binary (S q)) (k : a < S n),
 prop_list v
       (fun x y : VectorDef.t binary (S l) =>
        eq_vector_binary (take _ H x) (take _ H y) = true) ->
        (take _ H (nth v (of_nat_lt k))) = y.

  intros.
    have : forall x,
   (fun x : t binary (S l) => eq_vector_binary (take (S q) H x) y = true) x ->
      (take (S q) H x)  = y.
   intros.
   by apply : lex_vec_eq.
  move => inhabit.

  pose (rewrite_prop_list H0  inhabit).
  by apply (nth_prop_list k) in p.
Qed.
*)

Theorem take_fold : forall n h q (H : q < S n), (match
          h in (VectorDef.t _ n)
          return (S q <= n -> VectorDef.t binary (S q))
        with
        | [] => False_rect (VectorDef.t binary (S q)) ∘ Nat.nle_succ_0 q
        | cons _ x n0 xs =>
            fun le : S q <= S n0 => x :: take q (le_S_n q n0 le) xs
        end H) = take _ H h.
  by trivial.
Qed.

Theorem binary_refl : forall a, equal_binary a a = true.
by elim.
Qed.

Theorem binary_eq : forall a b, equal_binary a b = true -> a = b.
move => a b.
by elim/@b_rect : a/b.
Qed.

Theorem binary_sym : forall a b, equal_binary a b = true -> equal_binary b a = true.
by elim.
Qed.

Theorem eqv_partial_refl : forall {n} t y (H : y < S n), eq_vec_partial_eqv t t H.
  intros.
  elim/@rect_leb : t/H.
  intros.
  simpl.
  elim/@caseS' : v.
  intros; simpl.
  apply : binary_refl.
  intros.
  elim/@case0 : v.
  apply : binary_refl.
  intros.
  intros; simpl; unfold ssr_have; simpl.
  constructor.
  apply : binary_refl.
  exact H0.
Qed.

(*
Theorem eqv_partial_1 : forall {n} v v' (H : 0 < S n), eq_vec_partial_eqv (cross_binary_vector v v') v' H.
  intros.
  elim/@rect_2S : v/v' H.
  intros.
  by simpl.
  intros.
    have : 0 < S n0.
    auto with arith.
  move => H3.
  pose (H H3).
  simpl.
  elim/@b_rect : a/b e.
  simpl.
  intros.
*)
Theorem cross_refl_take : forall n x y q (H : q < S n),
   take _ H x = take _ H y ->
       take _ H (cross_binary_vector x y) = take _ H y.
  intros; elim/@rect_leb : x/H y H0.
  intros; elim/@caseS' : y H0.
  intros.
  simpl in H0; apply (f_equal hd) in H0; simpl in H0; rewrite H0.
  by destruct h.
  intros; elim/@caseS' : y H0; elim/@case0 : v.
  intros; elim/@case0 : t H0.
  intros; apply (f_equal hd) in H0.
  simpl in H0; rewrite H0; by destruct h.
  intros; move : H1; elim/@caseS' : y0.
  intros; simpl in H1.
  do 2! rewrite take_fold in H1.
  set (f_equal tl H1); set (f_equal hd H1).
  pose (H0 t e); simpl in e0.
  rewrite e0; simpl.
  destruct h; simpl.
  do 2! rewrite take_fold; rewrite e1.
  trivial.
  do 2! rewrite take_fold; rewrite e1.
  trivial.
Qed.

(*
Theorem next_eqv : forall n q H H' h (v : t binary (S n)),
eq_vector_binary (take (S q) H h) (take (S q) H v) = true
  -> eq_vector_binary (take (S (S q)) H' h) (take (S (S q)) H' (cross_binary_vector h v)) = true.
  intros.
  elim/@rect_leb : h/H v H' H0.
  intros.
  elim/@caseS' : v0 H0.
  intros.
  elim/@caseS' : v H0.
  elim/@caseS' : t.
  intros.
  elim/@b_rect : a/h H0.
  intros.
  apply lex_vec_eq in H0.


  elim/@b_rect : h1/h0 H0.

  inversion H'.
  inversion H2.
  intros.

  elim/@b_rect : x/y H0.
  *)


Theorem sym_eqv : forall {n} (h v : t binary (S n)) y (H : y < S n),
    eq_vec_partial_eqv h v H -> eq_vec_partial_eqv v h H.
  intros.
  elim/@rect_leb : h/H v H0.
  intros.
  elim/@caseS' : v0 H0.
  intros.
  simpl in *.
  elim/@caseS' : v H0.
  elim/@caseS' : t.
  intros.
  simpl in *.
  destruct H0.
  by elim/@b_rect : h/a.

  intros.
  elim/@case1 : v0 H0.
  elim/@case0 : v.
  intros; by apply : binary_sym.
  intros.
  elim/@caseS' : v0 H1.
  intros.
  destruct H1.
  simpl in *.
  unfold ssr_have.
  simpl.
  constructor.
  apply : (binary_sym H1).
  exact (H0 _ H2).
Qed.

(*
Theorem trans_Seqv : forall {n} (h v a : t binary (S n)) y (H : y < S n) (H' : S y < S n),
    eq_vec_partial_eqv a h H -> eq_vec_partial_eqv (cross_binary_vector a v) v H' ->
   eq_vec_partial_eqv (cross_binary_vector h (cross_binary_vector a v)) (cross_binary_vector a v) H'.
  intros.
  elim/@rect_leb : h/H v a H' H0 H1.
  intros.
  elim/@caseS' : v0 H1 H0.
  elim/@caseS' : a0.
  intros.
  elim/@b_rect : h/a H0 H1.
  intros.
  destruct h0.
  simpl in *; unfold ssr_have in *; simpl in *.

  by destruct h0.
  intros.
  by destruct h0.
  intros.
  destruct h0.
  simpl in *; unfold ssr_have in *; simpl in *.

  by [].
  *)

Theorem trans_Seqv : forall {n} (h v z : t binary (S n)) y (H : y < S n),
    eq_vec_partial_eqv h v H -> eq_vec_partial_eqv z h H -> eq_vec_partial_eqv z v H.
  intros.
  elim/@rect_leb : h/H v z H0 H1.
  intros.
  elim/@caseS' : v0 H0.
  elim/@caseS' : z H1.
  intros.
  simpl in *.
  elim/@caseS' : v H0 H1.
  elim/@caseS' : t.
  elim/@caseS' : t0.
  intros.
  rewrite (binary_eq H1).
  rewrite (binary_eq H0).
  by apply : binary_refl.
  intros.
  elim/@case1 : v0 H0.
  elim/@case1 : z H1.
  elim/@case0 : v.
  intros.
  simpl in *.

Admitted.

Theorem partial_0 : forall {n} (h v : t binary (S n)) (H : 0 < S n),
   eq_vec_partial_eqv (cross_binary_vector h v) v H.
Admitted.


Theorem partial_eqv_S : forall {n} (h v : t binary (S n)) y (H : y < S n) (H' : (S y) < S n),
    eq_vec_partial_eqv v h H -> eq_vec_partial_eqv (cross_binary_vector v h) h H'.
  intros.
  apply sym_eqv in H0.
  elim/@rect_leb : h/H v H' H0.
  intros.
  elim/@caseS' : v0 H0.
  intros.
  simpl in *.
  elim/@b_rect : a/h H0.
  simpl.
  unfold ssr_have.
  simpl.
  intros.
  constructor.
  apply : binary_refl.
  apply : partial_0.
  constructor.
  apply : binary_refl.
  apply : partial_0.
  constructor.
  apply : binary_refl.
  inversion H0.
  intros.
  inversion H0.
  intros.
  inversion H'; inversion H2.
  intros.
  elim/@caseS' : v0 H1.
  move => h t H1'.
  simpl in H1'.
  unfold ssr_have in H1'.
  simpl in H1'.
  destruct H1'.
  pose (H0 t (le_S_n (S (S y0)) (S n0) H') H2).
  by elim/@b_rect : a/h H1.
Qed.


Theorem cross_cons : forall {n} (v : t binary (S n)) t0 h0, (cross_binary_vector v (h0 :: t0)) = h0 :: (tl (cross_binary_vector v (h0 :: t0))).
Admitted.

Theorem trans_eqv : forall {n} (h v z : t binary (S n)) y (H : y < S n) (H' : S y < S n),
    eq_vec_partial_eqv h v H -> eq_vec_partial_eqv v z H ->
     eq_vec_partial_eqv (cross_binary_vector h z) (cross_binary_vector v z) H'.
  intros.

  elim/@rect_leb : h/H v z H' H1 H0.
  intros.

  elim/@caseS' : v0 H0 H1.
  elim/@caseS' : z.
  intros.
  simpl in *;unfold ssr_have in *; simpl in *.
  elim/@b_rect : a/h0 H0 H1.
  destruct h.
  simpl.
  intros.
  elim/@caseS' : t0 H0.
  elim/@caseS' : t H1.
  intros.
  simpl in *.
  destruct n0.
  elim/@case1 : v H1 H0.
  intros.
  elim/@case0 : t H1.
  elim/@case0 : t0.
  intros.
  simpl in *.
  elim/@b_rect : h/h0 H0 H1.
  intros.
  destruct h1.
  unfold ssr_have.
  simpl.
  unfold ssr_have in *;simpl.
  by constructor.
  by constructor.
  by constructor.
  by constructor.
  by constructor.
  by constructor.

  intros.
  simpl in *.
  unfold ssr_have; simpl in *.
  constructor.
  trivial.
  admit.
  intros.
  destruct h.
  simpl in *; unfold ssr_have in *; simpl in *.
  constructor.
  trivial.
  admit.
  simpl in *; unfold ssr_have in *; simpl in *.
  constructor.
  trivial.
  inversion H1.
  intros.
  destruct h.
  simpl in *; unfold ssr_have in *; simpl in *.
  inversion H0.
  inversion H0.
  destruct h.
  intros.
  inversion H0.
  intros.
  inversion H0.
  intros.
  inversion H'.
  inversion H3.
  intros.
  elim/@caseS' : v0 H1 H2.
  elim/@caseS' : z.
  intros.
  elim/@b_rect : a/h H1 H2.
  destruct h0.
  intros.
    simpl in *; unfold ssr_have in *; simpl in *.
  destruct H1.
  inversion H1.
  intros.
    simpl in *; unfold ssr_have in *; simpl in *.
  destruct H1.
  destruct H2.
  constructor.
  trivial.
  by apply (H0 t0 t (le_S_n (S (S y0)) (S n0) H') H3 H4).
  intros.
      simpl in *; unfold ssr_have in *; simpl in *.
  destruct h0.
      simpl in *; unfold ssr_have in *; simpl in *.
    constructor.
  trivial.
    destruct H1.
  destruct H2.
  by apply (H0 t0 t (le_S_n (S (S y0)) (S n0) H') H3 H4).
  intros.
  destruct H1.
  inversion H1.
  intros.
       simpl in *; unfold ssr_have in *; simpl in *.
  destruct h0.
      destruct H1.
  destruct H2.
         simpl in *; unfold ssr_have in *; simpl in *.
  inversion H2.
  destruct H1.
  inversion H1.
  intros.
  destruct h0.
  intros.
           simpl in *; unfold ssr_have in *; simpl in *.
  destruct H1.
  inversion H1.
  destruct H2.
  inversion H2.
Admitted.

Theorem eqv_seq : forall {n} y (v v' : t binary (S n)) (H : S y < S n)  (H' : y < S n),
    eq_vec_partial_eqv v v' H -> eq_vec_partial_eqv v v' H'.
  intros.
  elim/@rect_leb : v/H' v' H H0.
  intros.
  elim/@caseS' : v' H1.
  simpl; unfold ssr_have; simpl.
  intros.
  elim/@b_rect : a/h H1.
  by simpl.
  by simpl.
  intros; inversion H1; inversion H2.
  intros; inversion H1; inversion H2.
  intros; inversion H0; inversion H3.
  intros.
   have : S y0 < S n0.
   auto with arith.
  move => H4.
  elim/@caseS' : v' H2.
  intros.
  simpl in *; unfold ssr_have in *; simpl in *.
  destruct H2.
  pose (H0 t (le_S_n (S (S y0)) (S n0) H1) H3).
  by constructor.
Qed.


Theorem pure_0_cross : forall {n} (v v0 t t0 : t binary (S n)) (H : 0 < S n),
   eq_vec_partial_eqv t t0 H ->
        eq_vec_partial_eqv (cross_binary_vector v t) (cross_binary_vector v0 t0) H.
  intros.
  apply : (@trans_Seqv _ _ _ (cross_binary_vector v t) _ _ (sym_eqv (partial_0 v0 t0 H)) (sym_eqv (@trans_Seqv _ _ _ t0 _ _ (sym_eqv (partial_0 v t H)) (sym_eqv H0)))).
Qed.

(*
Theorem g_f : forall {n} y (a z v v' : t binary (S n)) (H : y < S n) (H' : S y < S n),
    eq_vec_partial_eqv a z H ->
         eq_vec_partial_eqv v v' H' ->
             eq_vec_partial_eqv (cross_binary_vector a v) (cross_binary_vector z v') H'.

 intros.
 elim/@rect_leb : a/H z v v' H' H0 H1.
 intros.
 elim/@caseS' : z H0.
 elim/@caseS' : v0 H1.
 elim/@caseS' : v'.
 intros.
 simpl in *; unfold ssr_have in *; simpl in *.
 elim/@b_rect : a/h0 H1 H0.
 elim/@b_rect : h/h1.
 intros.
 simpl in *; unfold ssr_have in *; simpl in *.
 constructor.
 trivial.
 destruct H1.
 apply : pure_0_cross.
 exact H2.
 intros.
 inversion H0.
 intros.
 inversion H0.
 intros.
 destruct H1.
 inversion H1.
 elim/@b_rect : h/h1.
 intros.
 inversion H0.
 intros.
 destruct H1.
 simpl in *; unfold ssr_have in *; simpl in *.
 constructor.
 trivial.
 apply : pure_0_cross.
 exact H2.
 intros.
 inversion H0.
 destruct H1.
 inversion H1.
 intros.
 inversion H0.
 elim/@b_rect : h/h1.
 intros.
 destruct H1.
 inversion H1.
 intros.
 inversion H0.
 intros.
 inversion H0.
 intros.
 destruct H1.
 simpl in *; unfold ssr_have in *; simpl in *.
 constructor.
 trivial.
 apply :

*)

Theorem cross_eqv_refl : forall {n} y (a c v : t binary (S n)) (H : y < S n) (H' : y < S n),
    eq_vec_partial_eqv a c H ->
         eq_vec_partial_eqv (cross_binary_vector a a) v H' ->
           eq_vec_partial_eqv (cross_binary_vector a c) v H'.
  intros.
  elim/@rect_leb : a/H v c H0 H' H1.
     intros.
  elim/@caseS' : v H0 H1.
  elim/@caseS' : c.
    intros.
  simpl in *.
  elim/@b_rect : a/h H0 H1.
  intros.
  intros.
  simpl in *.
  destruct n0.
  simpl in *.
  exact H1.
  simpl in *.
  exact H1.
  intros.
  simpl in *.
  exact H1.
  intros.
  simpl in *.
  elim/@caseS' : v0 H1.
  intros.
  simpl in *.
  destruct h.
  inversion H0.
  trivial.
  intros.
  inversion H0.
  intros.
  elim/@case0 : v H0 H1.
  elim/@caseS' : v0; elim/@caseS' : c.
  move => h; elim/@case0.
  intros; simpl in *.
  elim/@b_rect : a/h H0 H1.
  by destruct h0.
  by destruct h0.
  by destruct h0.
  by destruct h0.
    intros.
  elim/@caseS' : v0 H1 H2; elim/@caseS' : c.
  intros.
  simpl in *.
  unfold ssr_have in *.
  simpl in H1.
  destruct H1.
  pose (H0 t0 t H3).
  elim/@b_rect : a/h H1 H0 H2 e.
  intros.
  simpl in *.
  unfold ssr_have in *.
  simpl in *.
  destruct H2.
  apply e in H4.
  exact (conj H2 H4).
  intros.
  destruct H2.
  apply e in H4.
  exact (conj H2 H4).
  intros.
  inversion H1.
  intros.
  inversion H1.
Qed.

Theorem cross_eq_sym : forall {n} y (a c v : t binary (S n)) (H : y < S n),
    eq_vec_partial_eqv a c H ->
         eq_vec_partial_eqv (cross_binary_vector c a) v H ->
             eq_vec_partial_eqv (cross_binary_vector a c) v H.

  intros.
  elim/@rect_leb : a/H v c H0 H1.
  intros.
  elim/@caseS' : v H0 H1.
  elim/@caseS' : c.
  intros.
  simpl in *.
  elim/@b_rect : a/h H0 H1.
  intros.
  destruct n0.
  simpl in *.
  exact H1.
  simpl in *.
  exact H1.
  intros.
  simpl in *.
  exact H1.
  intros.
  simpl in *.
  elim/@caseS' : v0 H1.
  intros.
  simpl in *.
  destruct h.
  inversion H1.
  inversion H0.
  intros.
  inversion H0.
  intros.
  elim/@case0 : v H0 H1.
  elim/@caseS' : v0; elim/@caseS' : c.
  move => h; elim/@case0.
  intros; simpl in *.
  elim/@b_rect : a/h H0 H1.
  by destruct h0.
  by destruct h0.
  by destruct h0.
  by destruct h0.
  intros.
  elim/@caseS' : v0 H1 H2; elim/@caseS' : c.
  intros.
  simpl in *.
  unfold ssr_have in *.
  simpl in H1.
  destruct H1.
  pose (H0 t0 t H3).
  elim/@b_rect : a/h H1 H0 H2 e.
  intros.
  simpl in *.
  unfold ssr_have in *.
  simpl in *.
  destruct H2.
  apply e in H4.
  exact (conj H2 H4).
  intros.
  destruct H2.
  apply e in H4.
  exact (conj H2 H4).
  intros.
  inversion H1.
  intros.
  inversion H1.
Qed.

Theorem take_eqv : forall n q (x y : t binary (S n)) (H : q < S n),
    take _ H x = take _ H y -> eq_vec_partial_eqv x y H.
  intros.
  elim/@rect_leb : x/H y H0.
  intros.
  elim/@caseS' : y H0.
  intros.
  simpl in *.
  apply (f_equal hd) in H0.
  simpl in H0.
  rewrite H0.
  apply : binary_refl.
  intros.
  elim/@case0 : v H0.
  elim/@case1 : y.
  intros.
  simpl in *.
  apply (f_equal hd) in H0.
  simpl in H0.
  rewrite H0.
  apply : binary_refl.
  intros.
  elim/@caseS' : y0 H1.
  move => h k H1.
  simpl in H1.
  pose (f_equal hd H1).
  pose (f_equal tl H1).
  simpl in e.
  simpl in e0.
  pose (H0 k e0).
  simpl.
  unfold ssr_have; simpl.
  constructor.
  rewrite e.
  apply : binary_refl.
  exact e1.
Qed.

Theorem take_eqv' : forall n q (x y : t binary (S n)) (H : q < S n),
    eq_vec_partial_eqv x y H -> take _ H x = take _ H y.
 intros.
  elim/@rect_leb : x/H y H0.
  intros.
  elim/@caseS' : y H0.
  intros.
  simpl in *.
  apply (binary_eq) in H0.
  rewrite H0.
  apply : eq_refl.
  intros.
  elim/@case0 : v H0.
  elim/@case1 : y.
  intros.
  simpl in *.
  apply (binary_eq) in H0.
  simpl in H0.
  rewrite H0.
  apply : eq_refl.
  intros.
  elim/@caseS' : y0 H1.
  move => h k H1.
  simpl in H1.
  unfold ssr_have in H1.
  simpl in H1.
  destruct H1.
  apply binary_eq in H1.
  rewrite H1.
  pose (H0 k H2).

  simpl.
  simpl in e.
  by rewrite e.
Qed.

Theorem take_cross : forall n q (x y x' y' : t binary (S n)) (H : q < S n) (H' : S q < S n),
    take _ H x = take _ H x' /\ take _ H' y = take _ H' y' ->
    take _ H' (cross_binary_vector x y) = take _ H' (cross_binary_vector x' y').
  intros.
  destruct H0.
  elim/@rect_leb : x/H y x' y' H' H0 H1.
  intros.
  elim/@caseS' : y H1.
  elim/@caseS' : x' H0.
  elim/@caseS' : y'.
  intros.
  elim/@b_rect : a/h1 H0 H1.
  elim/@b_rect : h/h0.
  intros.
  apply : take_eqv'.
  apply take_eqv in H0.
  apply take_eqv in H1.
  simpl in *; unfold ssr_have in *; simpl in *.
  destruct H1.
  constructor.
  trivial.
  apply : pure_0_cross.
  exact H2.
  admit.
  admit.
  admit.
  admit.
  intros.
  elim/@b_rect : h/h0 H0 H1.
  admit.
  admit.
  admit.
  intros.
    apply : take_eqv'.
  apply take_eqv in H0.
  apply take_eqv in H1.
  simpl in *; unfold ssr_have in *; simpl in *.
  destruct H1.
  constructor.
  trivial.
Admitted.


Theorem eqv_succ : forall {n q} (h a h0 : t binary (S n)) (H : q < S n) (H' : S q < S n),
 eq_vec_partial_eqv h a H /\ eq_vec_partial_eqv a h0 H
   -> eq_vec_partial_eqv (cross_binary_vector h (cross_binary_vector a h0))
  (cross_binary_vector a h0) H'.

  intros.
  destruct H0.
  elim/@rect_leb : h/H H' a h0 H0 H1.
  intros.
  elim/@caseS' : a0 H0 H1.
  elim/@caseS' : h0.
  intros.
  elim/@b_rect : h0/h H0 H1.
  intros.
  destruct a.
  simpl in *.
  inversion H0.
  simpl in *; unfold ssr_have in *; simpl in *.
  constructor.
  trivial.
  apply : pure_0_cross.
  apply : partial_0.
  intros.
  destruct a.
  simpl in *; unfold ssr_have in *; simpl in *.
  constructor.
  trivial.
  apply : partial_0.
  intros.
  inversion H0.
  intros.
  simpl in *.
  inversion H1.
  intros.
  inversion H1.
  intros.
  elim/@case1 : a0 H0 H1.
  elim/@case1 : h0.
  elim/@case0 : v.
  intros.
  apply binary_eq in H0.
  apply binary_eq in H1.
  rewrite H0.
  rewrite H1.
  do 2! rewrite (cross_eq).
  apply : eqv_partial_refl.
  intros.
  elim/@caseS' : a0 H1 H2.
  elim/@caseS' : h0.
  intros.
  simpl in H1; unfold ssr_have in H1; simpl in H1.
  simpl in H2; unfold ssr_have in H2; simpl in H2.
  destruct H1.
  destruct H2.
  pose (H0 (le_S_n (S (S y)) (S n0) H') _ _ H3 H4).
  elim/@b_rect : h/h0 H1 H2.
  intros.
  destruct a.
  inversion H1.
  simpl; unfold ssr_have; simpl.
  by constructor.
  destruct a.
  intros.
  by constructor.
  intros.
  inversion H1.
  intros.
  inversion H2.
  intros.
  inversion H2.
Qed.

Theorem conservation_eqv : forall {n l} (v : t (t binary (S l)) (S n)) q (H : q < S l),
    prop_list v (fun x y => eq_vec_partial_eqv x y H)
      ->
     prop_list (binary_crossing' v) (fun x y => eq_vec_partial_eqv x y H).

Admitted.

Theorem conservation_eq : forall {n l} (v : t (t binary (S l)) (S n)) q (H : q < S l),
    prop_list v (fun x y => eq_vec_partial_eqv x y H) ->

      eq_vec_partial_eqv v[@F1] (binary_crossing' v)[@F1] H.

  intros.
  elim/@rectS : v H0.
  intros.
  simpl.
  apply : eqv_partial_refl.
  intros.
  destruct n0.
  elim/@case1 : v H1 H0.
  intros.
  simpl in *.
  destruct H1.
  apply : sym_eqv.
  apply : cross_eqv_refl.
  exact H1.
  rewrite (cross_eq).
  apply : eqv_partial_refl.
  elim/@caseS' : v H1 H0.
  intros.
  simpl in H1.
  destruct H1.
  pose (H0 H2).
  simpl.
  rewrite (vec_cons (binary_crossing' t)).
  simpl.
  simpl in e.
  rewrite -> (vec_cons (binary_crossing' t)) in e.
  simpl in e.
  apply : sym_eqv.
  apply : cross_eqv_refl.
  exact (@trans_Seqv _ _ _ a _ H e H1).
  rewrite (cross_eq).
  apply : eqv_partial_refl.
Qed.

Theorem conservation2_eq : forall {n l} (v : t (t binary (S l)) (S (S n))) q (H : q < S l),
    prop_list v (fun x y => eq_vec_partial_eqv x y H) ->

      eq_vec_partial_eqv v[@FS F1] (binary_crossing' v)[@F1] H.

 intros.
 elim/@caseS' : v H0.
 intros.
 simpl.
 rewrite (vec_cons (binary_crossing' _)).
 simpl.
 elim/@caseS' : t H0.
 intros.
 destruct H0.
 intros.
 destruct n.
 elim/@case0 : t H1.
 simpl.
 intros.
 apply : sym_eqv.
 apply : cross_eqv_refl.
 exact H0.
 rewrite (cross_eq).
 exact H0.
 intros.
 simpl.
 rewrite (vec_cons (binary_crossing' t)).
 simpl.
 apply : sym_eqv.
 apply : cross_eqv_refl.
 simpl in H1.
 pose (H1).
 move : c.
 rewrite -> (vec_cons t) in H1.
 simpl in H1.
 destruct H1.
 intros.
 apply : sym_eqv.
 apply : cross_eqv_refl.
 apply : sym_eqv.
 apply : (@trans_Seqv _ _ _ (binary_crossing' t)[@F1] _ _ (sym_eqv H1)).
 apply : sym_eqv.
 apply : conservation_eq.
 elim/@caseS' : t H1 H2 c.
 intros.
 simpl in c.
 destruct c.
 exact H4.
 rewrite (cross_eq).
 by apply : sym_eqv.
 by rewrite (cross_eq).
Qed.

Theorem induction_eqv : forall {n l} (v : t (t binary (S l)) (S n)) q (H : q < S l) (H' : (S q) < S l),
    prop_list v (fun x y => eq_vec_partial_eqv x y H)
      ->
     prop_list (binary_crossing' v) (fun x y => eq_vec_partial_eqv x y H').

  intros;elim/@rect_2per : v H0.
   + case.
      - simpl in *; unfold caseS'.
        intros; elim/@case1 : t H0 H1.
        intros; simpl in *.
        destruct H1.
        constructor.
        apply : eqv_succ.
        destruct H2.
        exact (conj H1 H2).
        apply (H0 H2).
    -  intros.
       destruct H1.
       simpl.
       rewrite (cons_bin _).
       unfold caseS'; simpl.
       constructor.
          have : 2 < S (S (S n0)).
          auto with arith.
       move => H3.
       apply : eqv_succ.
       constructor.
       exact H1.
       pose (H0 H2).
       pose (nth_prop_list (one_le _) H3 H2).
       pose (nth_prop_list (Nat.lt_0_succ _) (one_le _) p).
       simpl in e.

       rewrite -> (cons_bin) in e0.
       simpl in e0.
       pose (nth_prop_list (Nat.lt_0_succ _) (one_le _) p).

       apply : sym_eqv.
       apply : cross_eqv_refl.
       simpl in e1.
         elim/@caseS' : t H0 H2 H1 p e1 e e0.
       intros.
       simpl in H2.
       destruct H2.
       simpl.
       rewrite (vec_cons (binary_crossing' t)).
       simpl.
       simpl in e.
       apply : sym_eqv.
       apply : (@trans_Seqv _ _ _ (binary_crossing' t)[@F1]  _ _ (sym_eqv e)).
       apply : sym_eqv.
       apply : conservation_eq.
        elim/@caseS' : t H0 H2 H1 p e1 e H4 e0.
       intros.
       destruct H4.
       exact H5.
       rewrite (cross_eq).
       apply : sym_eqv (nth_prop_list (Nat.lt_0_succ _) (one_le _) H2).
       pose (H0 H2).
       simpl in p.
       rewrite -> (cons_bin) in p.
       simpl in p.
       exact p.

   + intros.
     simpl in *.
     constructor.
     destruct H0.
     by apply : partial_eqv_S.
     apply : eqv_partial_refl.

 +  intros.
    apply : eqv_partial_refl.
Qed.

Theorem convergent_binary_vector : forall {n l} (v : t (t binary (S l)) (S n)) q (H : S q < S l),
     prop_list (pow_' binary_crossing' (S (S q)) v) (fun x y => eq_vec_partial_eqv x y H).
  intros.
  induction q.
  intros.
  simpl.
  elim/@rectS : v.
  intros.
  simpl in *.
  apply : eqv_partial_refl.
  intros.
  simpl.
  destruct n0.
  elim/@case1 : v H0.
  intros.
  simpl in *.

  apply :

   have : q < S l.
   auto with arith.
  move => H3.
  pose (IHq H3).
  apply : (induction_eqv H p).

  elim/@rect_2per : v.
  admit.
  intros.
  simpl.
  elim/@rect_2S : h/v H.
  by simpl.
  intros.
  simpl in *.
  elim/@b_rect : a/b.
  simpl.
  pose (H (Nat.lt_0_succ _)).

  admit.
  rewrite (cons_bin _ (one_le _)) in e.

  pose (@partial_eqv_S _ a h0 _ H H' H2).


  pose (@trans_Seqv _ _ _ h _ _ H2 H1).

    have :  eq_vec_partial_eqv (cross_binary_vector h a) a H'.
    apply : sym_eqv.
    apply : trans_eqv.
    exact H1.
    by apply sym_eqv in H1.
  move => H4'.
  pose (@trans_Seqv _ _ _ (cross_binary_vector h a) _ _ H4' (eqv_partial_refl _ _)).
  pose (@trans_Seqv _ _ _ h _ _ H2 H1).
   have :  eq_vec_partial_eqv (cross_binary_vector a h0) a H.
    intros.
    apply : sym_eqv.
    apply : trans_eqv.
    exact H2.
    apply : eqv_partial_refl.
  move => H5'.

  pose (sym_eqv (@trans_Seqv _ _ _ (cross_binary_vector a h0)_ _ (sym_eqv e) H5')).

  apply : trans_eqv.

  (eqv_seq H H1).
  exact H2.

  rewrite (cons_bin).
  simpl.
  simpl in H2.
  move => H3.
  simpl in p.
    rewrite (tl_binary_cross).
    move => Hp.
    simpl.

  simpl.
  rewrite (cons_bin).

  pose (@rewrite_prop_list).

Theorem one_eqv_progress : forall {n l} (v : t (t binary (S l)) (S n)) q (H : q < S l) (H' : (S q) < S l),
    prop_list v (fun x y => eq_vec_partial_eqv x y H)
      ->
     prop_list (pow_' binary_crossing' n v) (fun x y => eq_vec_partial_eqv x y H').

  intros.
  elim/@rect_2per : v H0.
  intros.
  rewrite (cons_powtf').
  auto with arith.
  simpl.
  constructor.
  destruct H1.
  pose (H0 H2).
    have : 0 < S (S n0).
    auto with arith.
    have : 1 < S (S n0).
    auto with arith.
  move => H3' H2'.
  pose (nth_prop_list H2' H3' p).
  simpl in e.
   apply : trans_eqv.
  exact e.
   rewrite (cons_bin).
  auto with arith.
  rewrite (tl_bin).
  rewrite (tl_pow_f_bin).

  simpl.
  move => H3.
   have :   (pow_' binary_crossing' n0 (h :: a :: t))[@
        FS F1] = (pow_' binary_crossing' n0 (a :: t))[@F1].
   rewrite <- (hd_get').

   rewrite (vec_cons ((pow_' binary_crossing' n0 (h :: a :: t)))).
   simpl.
   destruct n0.
   trivial.
   simpl.
   rewrite (hd_bin).
   rewrite (tl_bin).
   rewrite (tl_pow_f_bin).
   by rewrite (cons_bin).

   pose(partial_eqv_S H' H1).
  move => eq2.
  rewrite eq2.

  destruct n0.
  admit.


    have : eq_vec_partial_eqv (cross_binary_vector h a) (pow_' binary_crossing' n0 (h :: a :: t))[@FS F1] H'.

    destruct n0.
    simpl.

    apply : (partial_eqv_S H' H1).
    simpl.
    rewrite (cons_bin).

    auto with arith.
    simpl.
    simpl in e.
    simpl in eq2.
    rewrite (cons_bin) in eq2.
    auto with arith.
    rewrite (cons_bin) in eq2.
    auto with arith.
    simpl in eq2.
    rewrite (tl_bin) in eq2.
    rewrite (tl_pow_f_bin) in eq2.
    rewrite (tl_bin).
    rewrite (tl_pow_f_bin).
    rewrite (cons_bin).
    rewrite (tl_bin).
    rewrite (tl_pow_f_bin).
    simpl.
    apply : trans_eqv.

    rewrite <- eq2.
  intros.
  simpl.
  apply : eqv_partial_refl.


Theorem one_eqv_progress : forall {n l} (v : t (t binary (S l)) (S n)) q (H : q < S l) (H' : (S q) < S l),
    prop_list v (fun x y => eq_vector_binary (take _ H x) (take _ H y) = true)
      ->
     prop_list (pow_f binary_crossing' n v) (fun x y => eq_vector_binary (take _ H' x) (take _ H' y) = true).
  intros.
  elim/@rect_2per : v H0.
  admit.
  intros.
  simpl in *.
  do 2! rewrite take_fold.
  do 2! rewrite take_fold in H0.

  intros.
  simpl in H1.
  destruct H1.
  apply H0 in H2.
  simpl.
  rewrite (cons_bin); intros.
  do 2! rewrite (tl_bin).
  rewrite -> binary_S.
  rewrite (tl_pow_f_bin).
  rewrite (cons_bin (binary_crossing' (pow_f binary_crossing' (S n0) (a :: t)))).
  move => Hyp1.
  do 2! rewrite (tl_bin).
  rewrite (tl_pow_f_bin).
  simpl.
  constructor.
    have : 0 < S (S n0).
    auto with arith.
  move => H3.
  pose (nth_prop_list H3 Hyp1 H2).
  simpl in e.
  fold @take.
  move : e H1.
  do 6! rewrite take_fold.
  move => e H1.
  apply lex_vec_eq in e.
  apply lex_vec_eq in H1.
  apply cross_refl_take in e.

  auto with arith.
    have : (pow_f binary_crossing' (S n0) (h :: a :: t)))[@F1]

  elim/@caseS' : t H0 H2.
  auto with arith.
  intros.


  do 2! rewrite (tl_bin).

Theorem one_eqv_progress : forall {n l} (v : pure_lex l n) q (H : q < S l) (H : (S q) < S l) b,
    prop_list v (eqv_progress b H)
      ->
   prop_list (pow_f binary_crossing' (S n) v) (eqv_progress b H)
   .
  intros.
  induction q.
  admit.

  elim/@rect_2per : v IHq H H0 H1.
  intros.
  pose (IHq
  simpl in *.
  destruct H2.
  destruct H3.
  rewrite -> binary_S.
  rewrite (cons_powtf' a h t).

  by simpl.

  intros.

  rewrite cons_powtf.
  auto with arith.
  simpl.
  constructor.
  rewrite -> binary_S.
  rewrite (cons_powtf' a h t).
  auto with arith.
  simpl.
  do 3! rewrite <- (hd_get').
  destruct n0.
  admit.
  rewrite (cons_bin (pow_f binary_crossing' (S n0) t)).
  simpl.
  intros.
  rewrite (hd_bin _).
  simpl.
  move => H3.
  unfold eqv_progress.
  simpl in H2.
  destruct H2.
  destruct H4.
  unfold eqv_progress in H2.
  unfold eqv_progress in H4.
  do 2! rewrite <- (hd_get').

  rewrite (hd_bin).
  intros;simpl in *.
  admit.
  auto with arith.
   auto with arith.
 auto with arith.

 simpl in *.
 destruct H2.
 pose (H H0 H1 H3).
 rewrite (cons_bin).
 simpl.
 constructor.
 unfold eqv_progress in *.
 destruct H3.


 rewrite -> (cons_bin _ Hyp0) in p.
 simpl in p.

 destruct p.
 rewrite -> (tl_bin) in H4.
  rewrite -> (tl_bin) in H4.

 rewrite (tl_pow_f_bin _) in H4.

 rewrite -> binary_S.
 rewrite cons_powtf.
 auto with arith.
 rewrite (cons_bin) in H3.
 rewrite -> (tl_bin) in H3.
 rewrite (tl_pow_f_bin _) in H3.
 simpl in H3.
 rewrite <- (hd_get') in H3.
  rewrite <- (hd_get') in H3.

 rewrite -> (hd_bin) in H3.

   have :       (cross_binary_vector
         (pow_f binary_crossing' n0 (a :: t))[@of_nat_lt
                                                 (Nat.lt_0_succ (S n0))]
         (pow_f binary_crossing' n0 (a :: t))[@of_nat_lt (one_le n0)])[@FS (of_nat_lt (lt_S_n q l H1))]  = b.
    have : of_nat_lt (Nat.lt_0_succ (S n0)) = F1.
      trivial.
    have : of_nat_lt (one_le n0) = FS F1.
      trivial.
   move => i i'.
   rewrite i.
   rewrite i'.

 rewrite <- H3.

 simpl.


   have : FS (of_nat_lt (lt_S_n q l H1)) = of_nat_lt H1.
   trivial.
 move => H3'.

 rewrite <- H3'.

 rewrite <- (hd_get').
 rewrite (hd_bin).
 simpl.

 destruct q.
 intros.
 simpl in *.
 constructor.
 unfold eqv_progress in *.
 destruct H1.
 exact (sym_binary_pair (sym_binary_pair ((sym_binary_pair H1 H2)) H2) H2).
 by destruct H1.
 intros.
 simpl in *.
 constructor.
 unfold eqv_progress.
 destruct H1.
 exact (sym_binary_pair (sym_binary_pair ((sym_binary_pair H1 H2)) H2) H2).
 by destruct H1.

 intros.
 by [].

 by destruct q.
 by simpl in *.


 simpl in *.
  destruct H2.
  destruct H3.
  rewrite (cons_bin).
  intros.
  simpl in *.
  constructor.
  unfold eqv_progress.
  unfold eqv_progress in H2.
  unfold eqv_progress in H3.
  rewrite (cons_bin).
  simpl.
  rewrite (cons_bin).
  simpl.
  rewrite -> (tl_bin).
  rewrite (tl_pow_f_bin).
  rewrite (cons_bin (pow_f binary_crossing' n0 t)).
  simpl.



  rewrite (cons_bin (pow_f binary_crossing' (S n0) t)).
  simpl.
  destruct n0.
  simpl.
  intros.

 (* intros; simpl.
    have : a[@of_nat_lt H1] = b /\
   prop_list t (fun v : VectorDef.t binary (S l) => v[@of_nat_lt H1] = b) .
    have : @FS _ (of_nat_lt (lt_S_n q l H1)) = of_nat_lt H1.
      by simpl.
    move => H3'.
    constructor.
    by rewrite <- H3'.
    by rewrite <- H3'.
  move => H4'.
  pose (H H0 H1 H4').
  simpl in p. *)


  rewrite (cons_bin).
  intros.
  do 2! rewrite -> (tl_bin).
  rewrite (tl_pow_f_bin _).
  rewrite -> binary_S.
  rewrite -> binary_S.
  rewrite -> binary_S.


intros.
simpl.
elim/@rect_leb : a/H.
intros.
destruct a.
right.
simpl.
rewrite (cross_eq _).
by unfold eqv_progress.
admit.
admit.
intros.
destruct H0.
destruct a.
right.
simpl in *.
rewrite (cross_eq _).
admit.
admit.
admit.
intros.
destruct H0.
left.
move : v H0.
elim/@rect_leb : a/H.
intros.
simpl.
rewrite (test (pow_f binary_crossing n0 v0)) in H0.
simpl in H0.
destruct n0.
move : H0.
elim/@caseS' : v0.
intros.
simpl in *.
move : H0.
elim/@case0 : t.
intros.
simpl in *.
rewrite (cross_eq _) in H0.
unfold eqv_progress in H0.
admit.
admit.
admit.
intros.
simpl in *.
rewrite (test  (pow_f binary_crossing n0 v0)) in H1.


unfold binary_crossing.
rewrite -> (shift_S _ _).

Theorem one_eqv_progress : forall {n l y} (v : pure_lex l n) (H : y < S l),
    eqv_progress (binary_crossing v) zero H \/ eqv_progress (binary_crossing v) one H.
intros.
elim/@rectS : v.
intros.
simpl.
rewrite (cross_eq _).
destruct (a[@of_nat_lt H]).
by left.
by right.
intros.
unfold binary_crossing.
simpl.
destruct H0.
left.
  have : nth (last v) (of_nat_lt H) = zero.
  intros.
  move : H0.
  elim/@rectS : v.
  intros.
  simpl in *.
  by rewrite (cross_eq _) in H0.
  intros.
  simpl in *.
  unfold binary_crossing in H1.
  simpl in H1.
  move : v H0 H1.
  elim/@rect_leb : a0/H; intros.
  simpl in *.
  admit.
  admit.


move : v H0.
elim/@rect_leb : a/H.
intros.
simpl in *.
unfold binary_crossing.


Fixpoint eq_walk_cross {l} (x y : t binary l) (k : nat) : t binary l.
destruct l.
refine (nil _).
elim/@caseS' : x.
elim/@caseS' : y.
intros.
refine (match k with
   |S ns => _
   |0 => _
  end).
refine (cons _ h0 _ t0).
refine (cons _ h _ (eq_walk_cross _ t t0 ns)).
Defined.



Definition take_eqv {l s} (x' y' : t binary (S l)) (E : S s <= S l) : nat :=
   eq_vec_binary_quantification (take _ E x') (take _ E y') 0.

Fixpoint quant_eqv {l n} (x' : pure_lex l n) (y : t binary (S l)) (s : nat) : S s <= S l -> Prop.
 elim/@rectS : x'.
 refine (fun x E => take_eqv x y E = S s).
 intros.
 refine (take_eqv a y H = S s \/ quant_eqv _ _ v y s H).
Defined.

Theorem quant_eqv_refl : forall {n q} (x : t binary (S n)) (e : S q <= S n),
  quant_eqv [x] x e.
  intros.
  Ltac f_trivial H := simpl in *; unfold H; by elim.
  elim/@rect_leb : x/e.
  f_trivial @take_eqv.
  f_trivial @take_eqv.
  intros; move : H H0; elim/@caseS' : v.
  destruct a.
  Ltac ignorance H0 h' := intros; simpl in *; unfold h' in *; simpl in *; rewrite -> H0;
                     by rewrite <- (plus_n_Sm _ _); rewrite <- (plus_n_O _).


  ignorance H0 @take_eqv.
  ignorance H0 @take_eqv.
Qed.

Theorem eq_progess_conserv : forall {n} (v2 : t binary n) q,
   eq_walk_cross v2 v2 q = v2.

 intros.
 move : v2.
 elim/@nat_double_ind  : q/n.
 intros;destruct n.
 by elim/@case0 : v2.
 intros;by elim/@caseS' : v2.
 intros;by elim/@case0 : v2.
 intros;elim/@caseS' : v2.
 by intros;simpl;rewrite (H t).
Qed.

Theorem cross_eq_partial_refl : True.

  have : forall a b, eq_walk_cross a b 0 = a.
    intros.
    move : b.
    destruct a.
    trivial.
    by elim/@caseS'.

  move => H10.
  have : forall n (v : t _ (S n)),
      pow_f (fun x => shiftin (hd x) (tl x)) n v =  v.
 intros.
 elim/@rectS : v.
 intros.
 by destruct n.
 intros.
 simpl.
  have : forall n (v : t _ (S n)), a :: pow_f (fun x => shiftin (hd x) (tl x)) (S n) v = pow_f (fun x => shiftin (hd x) (tl x)) (S n) (a :: v).
  intros.
  elim/@rectS : v0.
  intros.
  destruct n1.
  by [].
  by [].
  intros.
  simpl.

 elim/@case0 : t.
 trivial.
 elim/@caseS : t.
 intros.
 simpl.

 move => H3.
  have : forall n k (v : t (t binary (S k)) (S n)) q,
      shiftin (eq_walk_cross (hd v) (last v) (S q)) (tl (pow_f binary_crossing q v)) = pow_f binary_crossing q v.
    intros.
    move : v.
    elim/@nat_double_ind : n/q.
    intros.
    elim/@caseS' : v.
    intros.
    elim/@case0 : t.
    elim/@caseS' : h.
    simpl.
    induction n.
    simpl.
    intros.
    unfold binary_crossing.

    change (shiftin (cross_binary_vector (hd [h :: t]) (last [h :: t]))
  (tl [h :: t])) with [(cross_binary_vector (h :: t) (h :: t))].
    rewrite (cross_eq _).
    by rewrite (H3 _ _ _).
    intros.
    simpl in *.
    pose (IHn h t).
    rewrite -> (eq_progess_conserv _ (S n)).
    rewrite -> (eq_progess_conserv _ n) in e.
    rewrite <- e.
    unfold binary_crossing.
    rewrite <- (cross_eq _).

    intros.
    rewrite -> (cross_eq _).
      have : forall x k, last (shiftin x k) = x.
      intros.
      by induction k0.

    move => H4.
    rewrite (H4 _ _ _ _).
      have : forall (x : VectorDef.t _ 1) q,
          pow_f binary_crossing q x = x.
      intros.
      elim/@caseS' : x.
      intros.
      elim/@case0 : t0.
      induction q.
      simpl.
      unfold binary_crossing.
      simpl.
      by rewrite -> (cross_eq _).
      simpl.
      rewrite IHq.
      unfold binary_crossing.
      simpl.
      by rewrite -> (cross_eq _).

    move => H5.
    have :            (pow_f
              (fun x : pure_lex k 0 =>
               shiftin (cross_binary_vector (hd x) (last x)) (tl x)) n
              [h :: t]) = [h :: t].
    by apply : H5.
    move => H6.
    rewrite -> H6.
    simpl.
    clear e H6.
    destruct k.
    elim/@case0 : t.
    simpl.
    by destruct h.
    elim/@caseS : t.
    simpl.
    destruct h.
    intros; destruct n0.
    elim/@case0 : t.
    by destruct h.
    simpl.
    destruct h.
    by rewrite (cross_eq _).
    by rewrite (cross_eq _).
    intros; destruct n0.
    elim/@case0 : t.
    by destruct h.
    simpl.
    destruct h.
        by rewrite (cross_eq _).
    by rewrite (cross_eq _).
    intros.
    admit.
    intros.
    elim/@caseS' : v.
    intros.
    pose(H t).
    pose (pow_f binary_crossing (S m) (h :: t)).
    simpl in p.

     destruct n.
    elim/@case0 : t.
    simpl.
    by rewrite (cross_eq _).
    elim/@caseS' : t.
    intros.

    induction n0.
    unfold binary_crossing.

    intros; by elim/@b_rect : x/y.
    simpl in *.
    intros; rewrite <- (IHn0 x y).
    unfold binary_crossing.
    simpl.
    by elim/@b_rect : x/y.
    intros.
    simpl.
       have : forall a b, shiftin a [b] = [b; a].
       auto.
    move => H2.
    rewrite (H2 _ _ _) in H.

    simpl in *.
    destruct q.
    simpl in *.
    intros.
    pose (IHq x y).
    move : e.
    elim/@b_rect : x/y.
    trivial.
    trivial.

    intros.
    by elim/@b_rect : a/b.


 have : forall x n, hd x = hd (shiftin n x).
   intros.
   by elim/@rectS : x.

  have : forall {A} n (v : t A (S n)) k, (last (shiftin k v)) = k.
  intros.
  by elim/@rectS : v.

  have : forall e e1 k v, e = e1 /\ v = k :: (tl v) -> shiftin e v = k :: tl (shiftin e1 v).
  intros; destruct H.
  move : H0 H.
  elim/@rectS : v.
  intros; simpl.
  rewrite H; simpl in H.
  apply (f_equal hd) in H0; simpl in H0.
  by rewrite <- H0.
  intros; simpl in *; rewrite H1.
  pose (f_equal hd H0); simpl in e0; by rewrite e0.

  have : forall v, v = hd v :: tl v.
  move => t n.
  by elim/@rectS.

intros.

move : H v.
move => H v0.
elim/@rectS : v0.
intros.
destruct q.
rewrite (x3 _ _ _ _).
simpl.
by unfold binary_crossing.
simpl.
unfold binary_crossing.
apply : x0.
constructor.
trivial.
rewrite <- (x2 _ _ _ _).
rewrite -> (x1 _ _ _ _).

intros.
simpl.
generalize (pow_f
     (fun x0 : pure_lex l 1 =>
      shiftin (cross_binary_vector (hd x0) (last x0)) (tl x0)) q
     [a; a0]).
move => p.
  have : forall H p, tl p =
eq_walk_cross (hd (tl p)) (cross_binary_vector (hd p) (last p)) H
:: tl (tl p).
  intros.
  induction n0.
  rewrite (x3 _ _ _ _).
  apply : x.
  pose (IHn0 (le_Sn_le _ _ H0)).
  rewrite -> e.
  simpl in *.
    have : forall x y v, x = y -> x :: v = y :: v.
    congruence.
  apply.
  generalize (le_Sn_le (S n0) (S n1) H0).
  intros.
    have : forall p0 l0, eq_walk_cross (hd (tl p0)) (cross_binary_vector (hd p0) (last p0)) l0 =
eq_walk_cross
  (eq_walk_cross (hd (tl p0)) (cross_binary_vector (hd p0) (last p0)) l0)
  (cross_binary_vector (hd p0) (last p0)) l0.
  intros.

  elim/@caseS' : p1.
  clear l0.
  intros.
  move : t.
  simpl.

  elim/@rect_leb : h/l1.
  simpl.
  unfold caseS'.
  simpl.
  intros.
  elim/@caseS' : (last t).
  intros;elim/@b_rect : a1/h.
  simpl.
  rewrite (x3 _ _ _).
  by rewrite (x3 _ _ _).
   by rewrite (x3 _ _ _).
   by rewrite (x3 _ _ _).
 by rewrite (x3 _ _ _).
 intros.
   by rewrite (x3 _ _ _).
  intros.
 simpl in *.


Admitted.

Theorem crossing_walk : forall {l n q} (x : pure_lex l n) (E : S q <= S l),
  quant_eqv (pow_f binary_crossing q x) (hd x) E.

intros.
cbv in x.
elim/@rectS : x.
induction q.
intros.
simpl in *.
by simpl; rewrite (cross_eq _); apply : quant_eqv_refl.
admit.
intros.
simpl in *.
unfold quant_eqv.
Admitted.


Fixpoint EQ_vec {l n} (x : pure_lex l n) (y : t binary (S l)) : Prop.
refine (match x in (t _ (S n)) with
          |cons _ _ 0 k => match k with
                                  |cons _ _ _ _ => _
                                  |nil _ => _
                              end
          |cons _ _ (S n') _ => _
          end).

refine (eq_vector_binary t y).
exact idProp.
refine (eq_vector_binary t y /\ (EQ_vec _ _ t1 y)).
Defined.

Theorem totally_convergent :
   forall {l n} (x : pure_lex l n), EQ_vec (whole_crossing x) (hd (whole_crossing x)).
intros.
move : x.
induction l.
intros.
elim/@rectS : x.
intros.
elim/@caseS' : a.
intros.
simpl.
elim/@case0 : t.
simpl in *.
destruct h.
trivial.
trivial.
intros.
elim/@caseS' : a.
move : H.
elim/@caseS' : v.
intros.
move : H.
elim/@caseS' : h.
elim/@case0 : t0.

intros.
move : H.
elim/@case0 : t0.
intros.
unfold whole_crossing in *.
simpl in *.

pose(h :: t).
unfold whole_crossing.
simpl.

admit.
intros.
simpl in *.
unfold whole_crossing in *.
simpl in *.

intros.
simpl in *.


destruct l.



destruct v0.

by pose (lex_binary_eqv (lex' (cross_binary_vector (cross_binary_vector a a) (cross_binary_vector a a)))).
intros.


Instance SEnvironment : forall x y (k : t (SAgent x) (S y)),
   @Environment _ _ _ _ _ _ (
  fun x => t x (S y)) boundness get_agent (SAgent' x y) k (F' shift match_lex).
{
  constructor.
  exists 0.
  elim/@caseS : x0.
  unfold boundness.
  auto with arith.

   have :  boundness k 0.
   unfold boundness.
   auto with arith.
  move => H'.
   have :  boundness k y.
   unfold boundness.
   auto with arith.
  move => H2'.
  pose (@P' _ _ _ k boundness   (@perception (lex x) nat (SAgent x) cross_lex (lex_binary (n:=x))
     (t^~ (S y)) boundness (binary_lex x) (SAgent x)
     (SAgent' x y)) 0 y H' H2').
    have :  perception H' H2'.
    unfold  perception.
    simpl; unfold view.

  by rewrite ( Nat.eqb_eq  y y).
  auto.

  intros.
  unfold boundness in *.
  exists (0, y).
  exists (Nat.lt_0_succ y, @le_n (S y)).
  unfold view.
  simpl.
  apply : Nat.eqb_refl.

  intros.
  constructor;intros.
  destruct Pr.
  unfold view in PE0.
  unfold action_prop.
  unfold boundness in *.
  simpl in *.
  unfold action_prop.
  unfold get_agent.
  move : Px'0 Py'0 PE0.
  intros.
  apply andb_true_iff in PE0.
  destruct PE0.
  apply beq_nat_true in H.
  apply beq_nat_true in H0.
  subst.
  intros; apply : law1.

  simpl in *.
  unfold boundness in *.
  destruct Pr.
  simpl in *.
  unfold view in PE0.
  apply andb_true_iff in PE0.
  destruct PE0.
  apply beq_nat_true in H; apply beq_nat_true in H0.
  subst.

  unfold get_agent; unfold nth_order.
    have : of_nat_lt a = of_nat_lt Px'0.
    apply of_nat_lt_c.
  move => H2; rewrite H2.
  apply : law2.
}

Defined.

Instance SUniverse : forall x y (v : t (SAgent x) (S y)), @State _ _ _ _ _ _ (
  fun x => t x (S y)) boundness get_agent (SAgent' x y) shift match_lex v.
constructor.
intros.

constructor.
(*when P(0) for environment *)
apply : SEnvironment.
intros.
constructor.
(*when P k -> P (k + 1), for the environment *)
unfold boundness in *.
move => H2; exists y; auto with arith.

   (*need to simplify *)
   have :  boundness k 0.
   unfold boundness.
   auto with arith.
  move => H'.
   have :  boundness k y.
   unfold boundness.
   auto with arith.
  move => H2'.
  pose (@P' _ _ _ (match_lex (shift k)) boundness  (@perception (lex x) nat (SAgent x) cross_lex (lex_binary (n:=x))
     (t^~ (S y)) boundness (binary_lex x) (SAgent x)
     (SAgent' x y)) 0 y H' H2').
    have :  perception H' H2'.
    unfold  perception.
    simpl; unfold view.

  by rewrite ( Nat.eqb_eq  y y).
  intros; auto.

intros; unfold boundness in *; exists (0, y); exists (Nat.lt_0_succ y, @le_n (S y)).
unfold view; apply : Nat.eqb_refl.
intros; constructor; simpl.
intros; destruct Pr; simpl in *.
intros;unfold action_prop; unfold boundness in *; apply andb_true_iff in PE0.
destruct PE0.
apply beq_nat_true in H; apply beq_nat_true in H0; subst.
(*both law1 and law2 proofs of inductive interaction was straightfoward, once law1 and law2 were
    strong enough to generalization of any type obeying just the type constaint *)
apply : law1.
intros; destruct Pr; simpl in *.
intros; unfold boundness in *; apply andb_true_iff in PE0.
destruct PE0.
apply beq_nat_true in H; apply beq_nat_true in H0.
subst; apply : law2.
Defined.