Require Export fintype.
Require Import Vectors.Vector Lia.
Require Import Utils.Various_utils.
Import VectorNotations.

Section row.

Context {w : nat}.

Inductive row (nrow : nat) : Type :=
  | var_row : fin w -> (fin) (nrow) -> row (nrow)
  | abst : Vector.t (row ((S) nrow)) w -> row (nrow)
  | halt : row (nrow).

Fixpoint size {n} (r : row n) : nat:=
   match r with
   | abst _ t => S (vsum (map size t))
   | _ => 1
   end.

Fact lt_S {l k} : l < S k -> (l = k) + (l < k).
Proof. intros Hk. destruct (Compare_dec.lt_eq_lt_dec l k) as [[H|H]|H]; auto. lia.
Qed.

Lemma row_size_ind (P : forall nrow, row nrow -> Prop) :
  (forall nrow x, (forall mrow y, size y < size x -> P mrow y) -> P nrow x) ->
  forall nrow x, P nrow x.
Proof. intro H. intros. apply H. induction (size x); intros. lia. destruct (lt_S H0).
  -apply H. rewrite e. apply IHn.
  -apply IHn,l.
Qed.

Fact inSize {n} {t : Vector.t (row (S n)) w} {a} : In a t -> size a < size (abst _ t).
Proof. intro. cbn. assert (In (size a) (map size t)).
  { induction H. now apply In_cons_hd. now apply In_cons_tl. }
  pose (in_smaller _ _ H0). lia.
Qed.

Lemma row_vect_ind (P : forall nrow, row nrow -> Prop):
  (forall nrow (f : fin w) (f0 : fin nrow), P nrow (var_row nrow f f0)) ->
  (forall nrow (t : t (row (S nrow)) w), Forall (P (S nrow)) t -> P nrow (abst nrow t)) ->
  (forall nrow, P nrow (halt nrow)) ->
  forall nrow (r : row nrow), P nrow r.
Proof. intros Hv Ha Hh. eapply row_size_ind. destruct x; intros. 1,3: auto.
  apply Ha. apply Forall_forall. intros. apply H. now apply inSize.
Qed.

Lemma congr_abst { mrow : nat } { s0 : Vector.t (row ((S) mrow)) w } { t0 : Vector.t (row ((S) mrow)) w } (H1 : s0 = t0) : abst (mrow) s0 = abst (mrow) t0 .
Proof. congruence. Qed.

Lemma congr_halt { mrow : nat } : halt (mrow) = halt (mrow) .
Proof. congruence. Qed.

Definition upRen_row_row { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) ((S) (m)) -> (fin) ((S) (n)) :=
  (up_ren) xi.

Fixpoint ren_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) (s : row (mrow)) : row (nrow) :=
    match s return row (nrow) with
    | var_row (_) i s => (var_row (nrow) i) (xirow s)
    | abst (_) s0 => abst (nrow) (map (ren_row (upRen_row_row xirow)) s0)
    | halt (_) => halt (nrow)
    end.

Definition up_row_row { m : nat } { nrow : nat } (sigma : fin w -> (fin) (m) -> row (nrow)) : fin w -> (fin) ((S) (m)) -> row ((S) nrow) :=
  fun i => (scons) ((var_row ((S) nrow) i) (var_zero)) ((funcomp) (ren_row (shift)) (sigma i)).

Fixpoint subst_row { mrow : nat } { nrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (nrow)) (s : row (mrow)) : row (nrow) :=
    match s return row (nrow) with
    | var_row (_) i s => sigmarow i s
    | abst (_) s0 => abst (nrow) (map (subst_row (up_row_row sigmarow)) s0)
    | halt (_) => halt (nrow)
    end.

Definition upId_row_row { mrow : nat } (sigma : fin w -> (fin) (mrow) -> row (mrow)) (Eq : forall i x, sigma i x = (var_row (mrow) i) x) : forall i x, (up_row_row sigma) i x = (var_row ((S) mrow) i) x :=
  fun i n => match n with
  | Some fin_n => (ap) (ren_row (shift)) (Eq i fin_n)
  | None => eq_refl
  end.

(* Fixpoint idSubst_row { mrow : nat } (sigmarow : (fin) (mrow) -> row (mrow)) (Eqrow : forall x, sigmarow x = (var_row (mrow)) x) (s : row (mrow)) : subst_row sigmarow s = s :=
    match s return subst_row sigmarow s = s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((idSubst_row (up_row_row sigmarow) (upId_row_row (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma idSubst_row' { mrow : nat } (s : row (mrow)):
  forall (sigmarow : fin w -> (fin) (mrow) -> row (mrow)) (Eqrow : forall i x, sigmarow i x = (var_row (mrow) i) x), subst_row sigmarow s = s.
Proof. apply (row_vect_ind (fun n (s : row n) => forall (sig : fin w -> fin n -> row n) (Eq : forall (i : fin w) (x : fin n), sig i x = var_row n i x), subst_row sig s = s)); intros.
  -apply Eq.
  -apply congr_abst. rewrite (map_ext_in _ _ _ id). apply map_id. unfold id. apply Forall_forall.
    apply (Forall_impl _ (fun s : row (S nrow) => forall sig : fin w -> fin (S nrow) -> row (S nrow), (forall (i : fin w) (x : fin (S nrow)), sig i x = var_row (S nrow) i x) -> subst_row sig s = s)); auto.
    intros. apply H0. apply (upId_row_row _ Eq).
  -apply congr_halt.
Defined.
Definition idSubst_row { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (mrow)) (Eqrow : forall i x, sigmarow i x = (var_row (mrow)i ) x) (s : row (mrow)) : subst_row sigmarow s = s.
Proof. now apply idSubst_row'. Defined.

Definition upExtRen_row_row { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_row_row xi) x = (upRen_row_row zeta) x :=
  fun n => match n with
  | Some fin_n => (ap) (shift) (Eq fin_n)
  | None => eq_refl
  end.

(* Fixpoint extRen_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) (zetarow : (fin) (mrow) -> (fin) (nrow)) (Eqrow : forall x, xirow x = zetarow x) (s : row (mrow)) : ren_row xirow s = ren_row zetarow s :=
    match s return ren_row xirow s = ren_row zetarow s with
    | var_row (_) s => (ap) (var_row (nrow)) (Eqrow s)
    | abst (_) s0 => congr_abst ((extRen_row (upRen_row_row xirow) (upRen_row_row zetarow) (upExtRen_row_row (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma extRen_row' { mrow : nat } (s : row (mrow)) :
  forall (nrow : nat) (xirow : (fin) (mrow) -> (fin) (nrow)) (zetarow : (fin) (mrow) -> (fin) (nrow)) (Eqrow : forall x, xirow x = zetarow x), ren_row xirow s = ren_row zetarow s.
Proof. eapply (row_vect_ind (fun m r => forall n xi zeta (Eq : forall x, xi x = zeta x), ren_row xi r = ren_row zeta r)); intros.
  - apply (ap (var_row _ f) (Eq f0)).
  - apply congr_abst. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun r => forall (n : nat) (xi zeta : fin (S nrow) -> fin n), (forall x : fin (S nrow), xi x = zeta x) -> ren_row xi r = ren_row zeta r) ); auto.
    intros. apply H0. apply upExtRen_row_row,Eq.
  - apply congr_halt.
Defined.
Definition extRen_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) (zetarow : (fin) (mrow) -> (fin) (nrow)) (Eqrow : forall x, xirow x = zetarow x) (s : row (mrow)) : ren_row xirow s = ren_row zetarow s.
Proof. now apply extRen_row'. Defined.

Definition upExt_row_row { m : nat } { nrow : nat } (sigma : fin w -> (fin) (m) -> row (nrow)) (tau : fin w -> (fin) (m) -> row (nrow)) (Eq : forall i x, sigma i x = tau i x) : forall i x, (up_row_row sigma) i x = (up_row_row tau) i x :=
  fun i n => match n with
  | Some fin_n => (ap) (ren_row (shift)) (Eq i fin_n)
  | None => eq_refl
  end.

(* Fixpoint ext_row { mrow : nat } { nrow : nat } (sigmarow : (fin) (mrow) -> row (nrow)) (taurow : (fin) (mrow) -> row (nrow)) (Eqrow : forall x, sigmarow x = taurow x) (s : row (mrow)) : subst_row sigmarow s = subst_row taurow s :=
    match s return subst_row sigmarow s = subst_row taurow s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((ext_row (up_row_row sigmarow) (up_row_row taurow) (upExt_row_row (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma ext_row' { mrow : nat } (s : row (mrow)):
  forall (nrow : nat) (sigmarow : fin w -> (fin) (mrow) -> row (nrow)) (taurow : fin w -> (fin) (mrow) -> row (nrow)) (Eqrow : forall i x, sigmarow i x = taurow i x), subst_row sigmarow s = subst_row taurow s.
Proof. apply (row_vect_ind (fun m r => forall (nrow : nat) (sigmarow taurow : fin w -> fin m -> row nrow) (Eq: forall (i : fin w) (x : fin m), sigmarow i x = taurow i x), subst_row sigmarow r = subst_row taurow r)); intros.
  - apply Eq.
  - apply congr_abst. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun r : row (S nrow) => forall (nrow0 : nat) (sigmarow taurow : fin w -> fin (S nrow) -> row nrow0), (forall (i : fin w) (x : fin (S nrow)), sigmarow i x = taurow i x) -> subst_row sigmarow r = subst_row taurow r)); auto.
    intros. apply H0. apply upExt_row_row,Eq.
  - apply congr_halt.
Defined.
Definition ext_row { mrow : nat } { nrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (nrow)) (taurow : fin w -> (fin) (mrow) -> row (nrow)) (Eqrow : forall i x, sigmarow i x = taurow i x) (s : row (mrow)) : subst_row sigmarow s = subst_row taurow s.
Proof. now apply ext_row'. Defined.

Definition up_ren_ren_row_row { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_row_row tau) (upRen_row_row xi)) x = (upRen_row_row theta) x :=
  up_ren_ren xi tau theta Eq.

(* Fixpoint compRenRen_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (rhorow : (fin) (mrow) -> (fin) (lrow)) (Eqrow : forall x, ((funcomp) zetarow xirow) x = rhorow x) (s : row (mrow)) : ren_row zetarow (ren_row xirow s) = ren_row rhorow s :=
    match s return ren_row zetarow (ren_row xirow s) = ren_row rhorow s with
    | var_row (_) s => (ap) (var_row (lrow)) (Eqrow s)
    | abst (_) s0 => congr_abst ((compRenRen_row (upRen_row_row xirow) (upRen_row_row zetarow) (upRen_row_row rhorow) (up_ren_ren (_) (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma compRenRen_row' m (s : row m):
  forall { krow : nat } { lrow : nat } (xirow : (fin) (m) -> (fin) (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (rhorow : (fin) (m) -> (fin) (lrow)) (Eqrow : forall x, ((funcomp) zetarow xirow) x = rhorow x), ren_row zetarow (ren_row xirow s) = ren_row rhorow s.
Proof. apply (row_vect_ind (fun m s => forall (krow lrow : nat) (xirow : fin m -> fin krow) (zetarow : fin krow -> fin lrow) (rhorow : fin m -> fin lrow) (Eq : forall x : fin m, (xirow >> zetarow) x = rhorow x), ren_row zetarow (ren_row xirow s) = ren_row rhorow s)); intros.
  - apply (ap (var_row lrow f) (Eq f0)).
  - apply congr_abst. rewrite map_map. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun s : row (S nrow) => forall (krow lrow : nat) (xirow : fin (S nrow) -> fin krow) (zetarow : fin krow -> fin lrow) (rhorow : fin (S nrow) -> fin lrow), (forall x : fin (S nrow), (xirow >> zetarow) x = rhorow x) -> ren_row zetarow (ren_row xirow s) = ren_row rhorow s)); auto.
    intros. apply H0. apply up_ren_ren,Eq.
  - apply congr_halt.
Defined.
Definition compRenRen_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (rhorow : (fin) (mrow) -> (fin) (lrow)) (Eqrow : forall x, ((funcomp) zetarow xirow) x = rhorow x) (s : row (mrow)) : ren_row zetarow (ren_row xirow s) = ren_row rhorow s.
Proof. now apply compRenRen_row'. Defined.

Definition up_ren_subst_row_row { k : nat } { l : nat } { mrow : nat } (xi : (fin) (k) -> (fin) (l)) (tau : fin w -> (fin) (l) -> row (mrow)) (theta : fin w -> (fin) (k) -> row (mrow)) (Eq : forall i x, ((funcomp) (tau i) xi) x = theta i x) : forall i x, ((funcomp) (up_row_row tau i) (upRen_row_row xi)) x = (up_row_row theta) i x :=
  fun i n => match n with
  | Some fin_n => (ap) (ren_row (shift)) (Eq i fin_n)
  | None => eq_refl
  end.

(* Fixpoint compRenSubst_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (taurow : (fin) (krow) -> row (lrow)) (thetarow : (fin) (mrow) -> row (lrow)) (Eqrow : forall x, ((funcomp) taurow xirow) x = thetarow x) (s : row (mrow)) : subst_row taurow (ren_row xirow s) = subst_row thetarow s :=
    match s return subst_row taurow (ren_row xirow s) = subst_row thetarow s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((compRenSubst_row (upRen_row_row xirow) (up_row_row taurow) (up_row_row thetarow) (up_ren_subst_row_row (_) (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma compRenSubst_row' m (s : row m):
  forall { krow : nat } { lrow : nat } (xirow : (fin) m -> (fin) (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (thetarow : fin w -> (fin) m -> row (lrow)) (Eqrow : forall i x, ((funcomp) (taurow i) xirow) x = thetarow i x), subst_row taurow (ren_row xirow s) = subst_row thetarow s.
Proof. apply (row_vect_ind (fun m s => forall (krow lrow : nat) (xirow : fin m -> fin krow) (taurow : fin w -> fin krow -> row lrow) (thetarow : fin w -> fin m -> row lrow) (Eq : forall (i : fin w) (x : fin m), (xirow >> taurow i) x = thetarow i x), subst_row taurow (ren_row xirow s) = subst_row thetarow s)); intros.
  - apply Eq.
  - apply congr_abst. rewrite map_map. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun s : row (S nrow) => forall (krow lrow : nat) (xirow : fin (S nrow) -> fin krow) (taurow : fin w -> fin krow -> row lrow) (thetarow : fin w -> fin (S nrow) -> row lrow), (forall (i : fin w) (x : fin (S nrow)), (xirow >> taurow i) x = thetarow i x) -> subst_row taurow (ren_row xirow s) = subst_row thetarow s)); auto.
    intros. apply H0. apply up_ren_subst_row_row,Eq.
  - apply congr_halt.
Defined.
Definition compRenSubst_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (thetarow : fin w -> (fin) (mrow) -> row (lrow)) (Eqrow : forall i x, ((funcomp) (taurow i) xirow) x = thetarow i x) (s : row (mrow)) : subst_row taurow (ren_row xirow s) = subst_row thetarow s.
Proof. now apply compRenSubst_row'. Defined.

Definition up_subst_ren_row_row { k : nat } { lrow : nat } { mrow : nat } (sigma : fin w -> (fin) (k) -> row (lrow)) (zetarow : (fin) (lrow) -> (fin) (mrow)) (theta : fin w -> (fin) (k) -> row (mrow)) (Eq : forall i x, ((funcomp) (ren_row zetarow) (sigma i)) x = theta i x) : forall i x, ((funcomp) (ren_row (upRen_row_row zetarow)) (up_row_row sigma i)) x = (up_row_row theta) i x :=
  fun i n => match n with
  | Some fin_n => (eq_trans) (compRenRen_row (shift) (upRen_row_row zetarow) ((funcomp) (shift) zetarow) (fun x => eq_refl) (sigma i fin_n)) ((eq_trans) ((eq_sym) (compRenRen_row zetarow (shift) ((funcomp) (shift) zetarow) (fun x => eq_refl) (sigma i fin_n))) ((ap) (ren_row (shift)) (Eq i fin_n)))
  | None => eq_refl
  end.

(* Fixpoint compSubstRen_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : (fin) (mrow) -> row (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (thetarow : (fin) (mrow) -> row (lrow)) (Eqrow : forall x, ((funcomp) (ren_row zetarow) sigmarow) x = thetarow x) (s : row (mrow)) : ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s :=
    match s return ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((compSubstRen_row (up_row_row sigmarow) (upRen_row_row zetarow) (up_row_row thetarow) (up_subst_ren_row_row (_) (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma compSubstRen_row' m (s : row m):
  forall { krow : nat } { lrow : nat } (sigmarow : fin w -> (fin) m -> row (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (thetarow : fin w -> (fin) m -> row (lrow)) (Eqrow : forall i x, ((funcomp) (ren_row zetarow) (sigmarow i)) x = thetarow i x), ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s.
Proof. apply (row_vect_ind (fun m s => forall (krow lrow : nat) (sigmarow : fin w -> fin m -> row krow) (zetarow : fin krow -> fin lrow) (thetarow : fin w -> fin m -> row lrow) (Eq: forall (i : fin w) (x : fin m), (sigmarow i >> ren_row zetarow) x = thetarow i x), ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s)); intros.
  - apply Eq.
  - apply congr_abst. rewrite map_map. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun s : row (S nrow) => forall (krow lrow : nat) (sigmarow : fin w -> fin (S nrow) -> row krow) (zetarow : fin krow -> fin lrow) (thetarow : fin w -> fin (S nrow) -> row lrow), (forall (i : fin w) (x : fin (S nrow)), (sigmarow i >> ren_row zetarow) x = thetarow i x) -> ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s)); auto.
   intros. apply H0. apply up_subst_ren_row_row,Eq.
  - apply congr_halt.
Defined.
Definition compSubstRen_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (thetarow : fin w -> (fin) (mrow) -> row (lrow)) (Eqrow : forall i x, ((funcomp) (ren_row zetarow) (sigmarow i)) x = thetarow i x) (s : row (mrow)) : ren_row zetarow (subst_row sigmarow s) = subst_row thetarow s.
Proof. now apply compSubstRen_row'. Defined.

(* Definition up_subst_subst_row_row { k : nat } { lrow : nat } { mrow : nat } (sigma : fin w -> (fin) (k) -> row (lrow)) (taurow : fin w -> (fin) (lrow) -> row (mrow)) (theta : fin w -> (fin) (k) -> row (mrow)) (Eq : forall i x, ((funcomp) (subst_row (taurow)) (sigma i)) x = theta i x) : forall i x, ((funcomp) (subst_row (up_row_row taurow)) (up_row_row sigma i)) x = (up_row_row theta) i x :=
  fun i n => match n with
  | Some fin_n => (eq_trans) (compRenSubst_row (shift) (up_row_row taurow) ((funcomp) (up_row_row taurow) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_row taurow (shift) ((funcomp) (ren_row (shift)) taurow) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_row (shift)) (Eq fin_n)))
  | None  => eq_refl
  end.
 *)
Definition up_subst_subst_row_row { k : nat } { lrow : nat } { mrow : nat } (sigma : fin w -> (fin) (k) -> row (lrow)) (taurow : fin w -> (fin) (lrow) -> row (mrow)) (theta : fin w -> (fin) (k) -> row (mrow)) (Eq : forall i x, ((funcomp) (subst_row (taurow)) (sigma i)) x = theta i x) : forall i x, ((funcomp) (subst_row (up_row_row taurow)) (up_row_row sigma i)) x = (up_row_row theta) i x.
Proof. intros i [j |]. 2: apply eq_refl. apply (eq_trans (compRenSubst_row ↑ (up_row_row taurow) (fun i => ↑ >> up_row_row taurow i) (fun _ _ => eq_refl) (sigma i j) )).
  apply (eq_trans (eq_sym (compSubstRen_row taurow ↑ (fun i => taurow i >> ren_row ↑) (fun _ _ => eq_refl) (sigma i j)))).
  apply (ap (ren_row ↑)), Eq.
Defined.

(* Fixpoint compSubstSubst_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : (fin) (mrow) -> row (krow)) (taurow : (fin) (krow) -> row (lrow)) (thetarow : (fin) (mrow) -> row (lrow)) (Eqrow : forall x, ((funcomp) (subst_row taurow) sigmarow) x = thetarow x) (s : row (mrow)) : subst_row taurow (subst_row sigmarow s) = subst_row thetarow s :=
    match s return subst_row taurow (subst_row sigmarow s) = subst_row thetarow s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((compSubstSubst_row (up_row_row sigmarow) (up_row_row taurow) (up_row_row thetarow) (up_subst_subst_row_row (_) (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma compSubstSubst_row' m (s : row m) :
  forall { krow : nat } { lrow : nat } (sigmarow : fin w -> (fin) m -> row (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (thetarow : fin w -> (fin) (m) -> row (lrow)) (Eqrow : forall i x, ((funcomp) (subst_row taurow) (sigmarow i)) x = thetarow i x), subst_row taurow (subst_row sigmarow s) = subst_row thetarow s.
Proof. apply (row_vect_ind (fun m s => forall (krow lrow : nat) (sigmarow : fin w -> fin m -> row krow) (taurow : fin w -> fin krow -> row lrow) (thetarow : fin w -> fin m -> row lrow) (Eq : forall (i : fin w) (x : fin m), (sigmarow i >> subst_row taurow) x = thetarow i x), subst_row taurow (subst_row sigmarow s) = subst_row thetarow s)); intros.
  -apply Eq.
  -apply congr_abst. rewrite map_map. apply map_ext_in. apply Forall_forall.
    apply (Forall_impl _ (fun s : row (S nrow) => forall (krow lrow : nat) (sigmarow : fin w -> fin (S nrow) -> row krow) (taurow : fin w -> fin krow -> row lrow) (thetarow : fin w -> fin (S nrow) -> row lrow), (forall (i : fin w) (x : fin (S nrow)), (sigmarow i >> subst_row taurow) x = thetarow i x) -> subst_row taurow (subst_row sigmarow s) = subst_row thetarow s)); auto.
    intros. apply H0. apply up_subst_subst_row_row,Eq.
  -apply congr_halt.
Defined.
Definition compSubstSubst_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (thetarow : fin w -> (fin) (mrow) -> row (lrow)) (Eqrow : forall i x, ((funcomp) (subst_row taurow) (sigmarow i)) x = thetarow i x) (s : row (mrow)) : subst_row taurow (subst_row sigmarow s) = subst_row thetarow s.
Proof. now apply compSubstSubst_row'. Defined.

Definition rinstInst_up_row_row { m : nat } { nrow : nat } (xi : (fin) (m) -> (fin) (nrow)) (sigma : fin w -> (fin) (m) -> row (nrow)) (Eq : forall i x, ((funcomp) (var_row (nrow) i) xi) x = sigma i x) : forall i x, ((funcomp) (var_row ((S) nrow) i) (upRen_row_row xi)) x = (up_row_row sigma) i x :=
  fun i n => match n with
  | Some fin_n => (ap) (ren_row (shift)) (Eq i fin_n)
  | None => eq_refl
  end.

(* Fixpoint rinst_inst_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) (sigmarow : (fin) (mrow) -> row (nrow)) (Eqrow : forall x, ((funcomp) (var_row (nrow)) xirow) x = sigmarow x) (s : row (mrow)) : ren_row xirow s = subst_row sigmarow s :=
    match s return ren_row xirow s = subst_row sigmarow s with
    | var_row (_) s => Eqrow s
    | abst (_) s0 => congr_abst ((rinst_inst_row (upRen_row_row xirow) (up_row_row sigmarow) (rinstInst_up_row_row (_) (_) Eqrow)) s0)
    | halt (_)  => congr_halt 
    end. *)
Lemma rinst_inst_row' m (s : row m) :
  forall { nrow : nat } (xirow : (fin) (m) -> (fin) (nrow)) (sigmarow : fin w -> (fin) (m) -> row (nrow)) (Eqrow : forall i x, ((funcomp) (var_row (nrow) i) xirow) x = sigmarow i x), ren_row xirow s = subst_row sigmarow s.
Proof. apply (row_vect_ind (fun m s => forall (nrow : nat) (xirow : fin m -> fin nrow) (sigmarow : fin w -> fin m -> row nrow) (Eq : forall (i : fin w) (x : fin m), (xirow >> var_row nrow i) x = sigmarow i x), ren_row xirow s = subst_row sigmarow s)); intros.
  -apply Eq.
  -apply congr_abst. apply map_ext_in. apply Forall_forall.
   apply (Forall_impl _ (fun s : row (S nrow) => forall (nrow0 : nat) (xirow : fin (S nrow) -> fin nrow0) (sigmarow : fin w -> fin (S nrow) -> row nrow0), (forall (i : fin w) (x : fin (S nrow)), (xirow >> var_row nrow0 i) x = sigmarow i x) -> ren_row xirow s = subst_row sigmarow s)); auto.
    intros. apply H0. apply rinstInst_up_row_row,Eq.
  -apply congr_halt.
Defined.
Definition rinst_inst_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) (sigmarow : fin w -> (fin) (mrow) -> row (nrow)) (Eqrow : forall i x, ((funcomp) (var_row (nrow) i) xirow) x = sigmarow i x) (s : row (mrow)) : ren_row xirow s = subst_row sigmarow s.
Proof. now apply rinst_inst_row'. Defined.

Lemma rinstInst_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) : ren_row xirow = subst_row (fun i => (funcomp) (var_row (nrow) i) xirow) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_row xirow (_) (fun _ n => eq_refl) x)). Qed.

Lemma instId_row { mrow : nat } : subst_row (var_row (mrow)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_row (var_row (mrow)) (fun _ n => eq_refl) ((id) x))). Qed.

Lemma rinstId_row { mrow : nat } : @ren_row (mrow) (mrow) (id) = id .
Proof. exact ((eq_trans) (rinstInst_row ((id) (_))) instId_row). Qed.

Lemma varL_row { mrow : nat } { nrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (nrow)) : (fun i => (funcomp) (subst_row sigmarow) (var_row (mrow) i)) = sigmarow .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma varLRen_row { mrow : nat } { nrow : nat } (xirow : (fin) (mrow) -> (fin) (nrow)) : (fun i => (funcomp) (ren_row xirow) (var_row (mrow) i)) = (fun i => (funcomp) (var_row (nrow) i) xirow) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma compComp_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (s : row (mrow)) : subst_row taurow (subst_row sigmarow s) = subst_row (fun i => (funcomp) (subst_row taurow) (sigmarow i)) s .
Proof. exact (compSubstSubst_row sigmarow taurow (_) (fun _ n => eq_refl) s). Qed.

Lemma compComp'_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) : (funcomp) (subst_row taurow) (subst_row sigmarow) = subst_row (fun i => (funcomp) (subst_row taurow) (sigmarow i)) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_row sigmarow taurow n)). Qed.

Lemma compRen_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (s : row (mrow)) : ren_row zetarow (subst_row sigmarow s) = subst_row (fun i => (funcomp) (ren_row zetarow) (sigmarow i)) s .
Proof. exact (compSubstRen_row sigmarow zetarow (_) (fun _ n => eq_refl) s). Qed.

Lemma compRen'_row { krow : nat } { lrow : nat } { mrow : nat } (sigmarow : fin w -> (fin) (mrow) -> row (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) : (funcomp) (ren_row zetarow) (subst_row sigmarow) = subst_row (fun i => (funcomp) (ren_row zetarow) (sigmarow i)) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_row sigmarow zetarow n)). Qed.

Lemma renComp_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) (s : row (mrow)) : subst_row taurow (ren_row xirow s) = subst_row (fun i => (funcomp) (taurow i) xirow) s .
Proof. exact (compRenSubst_row xirow taurow (_) (fun _ n => eq_refl) s). Qed.

Lemma renComp'_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (taurow : fin w -> (fin) (krow) -> row (lrow)) : (funcomp) (subst_row taurow) (ren_row xirow) = subst_row (fun i => (funcomp) (taurow i) xirow) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_row xirow taurow n)). Qed.

Lemma renRen_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) (s : row (mrow)) : ren_row zetarow (ren_row xirow s) = ren_row ((funcomp) zetarow xirow) s .
Proof. exact (compRenRen_row xirow zetarow (_) (fun n => eq_refl) s). Qed.

Lemma renRen'_row { krow : nat } { lrow : nat } { mrow : nat } (xirow : (fin) (mrow) -> (fin) (krow)) (zetarow : (fin) (krow) -> (fin) (lrow)) : (funcomp) (ren_row zetarow) (ren_row xirow) = ren_row ((funcomp) zetarow xirow) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_row xirow zetarow n)). Qed.

End row.

Arguments var_row {w} {nrow}.

Arguments abst {w} {nrow}.

Arguments halt {w} {nrow}.

(* Global Instance Subst_row { mrow : nat } { nrow : nat } : Subst1 ((fin) (mrow) -> row (nrow)) (row (mrow)) (row (nrow)) := @subst_row (mrow) (nrow) . *)

(* Global Instance Ren_row { mrow : nat } { nrow : nat } : Ren1 ((fin) (mrow) -> (fin) (nrow)) (row (mrow)) (row (nrow)) := @ren_row (mrow) (nrow) . *)

(* Global Instance VarInstance_row { mrow : nat } : Var ((fin) (mrow)) (row (mrow)) := @var_row (mrow) . *)

(* Notation "x '__row'" := (var_row x) (at level 5, format "x __row") : subst_scope. *)

(* Notation "x '__row'" := (@ids (_) (_) VarInstance_row x) (at level 5, only printing, format "x __row") : subst_scope. *)

(* Notation "'var'" := (var_row) (only printing, at level 1) : subst_scope. *)

Class Up_row X Y := up_row : X -> Y.

(* Notation "↑__row" := (up_row) (only printing) : subst_scope. *)

(* Notation "↑__row" := (up_row_row) (only printing) : subst_scope. *)

(* Global Instance Up_row_row { m : nat } { nrow : nat } : Up_row (_) (_) := @up_row_row (m) (nrow) . *)

(* Notation "s  sigmarow " := (subst_row sigmarow s) (at level 7, left associativity, only printing) : subst_scope. *)

(* Notation " sigmarow " := (subst_row sigmarow) (at level 1, left associativity, only printing) : fscope. *)

(* Notation "s ⟨ xirow ⟩" := (ren_row xirow s) (at level 7, left associativity, only printing) : subst_scope. *)

(* Notation "⟨ xirow ⟩" := (ren_row xirow) (at level 1, left associativity, only printing) : fscope. *)

Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2(* ,  Subst_row,  Ren_row,  VarInstance_row *).

Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2(* ,  Subst_row,  Ren_row,  VarInstance_row *) in *.

Ltac asimpl' := repeat first [progress rewrite ?instId_row| progress rewrite ?compComp_row| progress rewrite ?compComp'_row| progress rewrite ?rinstId_row| progress rewrite ?compRen_row| progress rewrite ?compRen'_row| progress rewrite ?renComp_row| progress rewrite ?renComp'_row| progress rewrite ?renRen_row| progress rewrite ?renRen'_row| progress rewrite ?varL_row| progress rewrite ?varLRen_row| progress (unfold up_ren, upRen_row_row, up_row_row)| progress (cbn [subst_row ren_row])| fsimpl].

Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.

Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.

Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).

Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_row in *| progress rewrite ?compComp_row in *| progress rewrite ?compComp'_row in *| progress rewrite ?rinstId_row in *| progress rewrite ?compRen_row in *| progress rewrite ?compRen'_row in *| progress rewrite ?renComp_row in *| progress rewrite ?renComp'_row in *| progress rewrite ?renRen_row in *| progress rewrite ?renRen'_row in *| progress rewrite ?varL_row in *| progress rewrite ?varLRen_row in *| progress (unfold up_ren, upRen_row_row, up_row_row in *)| progress (cbn [subst_row ren_row] in *)| fsimpl in *].

Ltac substify := auto_unfold; try repeat (erewrite rinstInst_row).

Ltac renamify := auto_unfold; try repeat (erewrite <- rinstInst_row).