Require Import Arith Lia Vector.
From Undecidability.Shared.Libs.PSL Require Import Vectors VectorForall.
From Undecidability.SOL.Util Require Import Syntax.
Require Import Undecidability.SOL.SOL.

Set Default Proof Using "Type".

#[global] Instance econs_subst_indi `{funcs_signature} : Econs _ _ := econs_indi term.
#[global] Instance econs_subst_func `{funcs_signature} ar : Econs _ _ := econs_ar ar function.
#[global] Instance econs_subst_pred `{preds_signature} ar : Econs _ _ := econs_ar ar predicate.


Class IdSubst X := ids : X.
Class Shift X := shift : X.

#[global] Instance var_indi' `{funcs_signature} : IdSubst term := var_indi.
#[global] Instance var_func' `{funcs_signature} : IdSubst ( ar, function ar) := var_func.
#[global] Instance var_pred' `{preds_signature} : IdSubst ( ar, predicate ar) := var_pred.

#[global] Instance shift_i `{funcs_signature} : Shift ( term) :=
   n var_indi (S n).

#[global] Instance shift_f `{funcs_signature} : Shift ( ar, function ar) :=
   ar n ar' if Nat.eq_dec ar ar' then @var_func _ (S n) ar' else @var_func _ n ar'.

#[global] Instance shift_p `{preds_signature} : Shift ( ar, predicate ar) :=
   ar n ar' if Nat.eq_dec ar ar' then @var_pred _ (S n) ar' else @var_pred _ n ar'.


Class Subst_i `{funcs_signature} X := subst_i : ( term) X X.
Class Subst_f `{funcs_signature} X := subst_f : ( ( ar, function ar)) X X.
Class Subst_p `{preds_signature} X := subst_p : ( ( ar, predicate ar)) X X.

Local Notation "X [ σ ]i" := (subst_i σ X) (at level 7, left associativity, format "X '/' [ σ ]i").
Local Notation "X [ σ ]f" := (subst_f σ X) (at level 7, left associativity, format "X '/' [ σ ]f").
Local Notation "X [ σ ]p" := (subst_p σ X) (at level 7, left associativity, format "X '/' [ σ ]p").

#[global] Instance subst_function `{funcs_signature} {ar} : Subst_f (function ar) := σf f match f with
  | var_func f σf f ar
  | f f
end.

#[global] Instance subst_term_i `{funcs_signature} : Subst_i term := fix subst_term_i σi t := match t with
  | var_indi x σi x
  | func f v func f (Vector.map (subst_term_i σi) v)
end.

#[global] Instance subst_term_f `{funcs_signature} : Subst_f term := fix subst_term_f σf t := match t with
  | var_indi x var_indi x
  | func f v func (subst_function σf f) (Vector.map (subst_term_f σf) v)
end.

#[global] Instance subst_predicate `{preds_signature} {ar} : Subst_p (predicate ar) := σp P match P with
  | var_pred P σp P ar
  | P P
end.

Definition up_i `{funcs_signature} (σi : term) := econs (var_indi 0) ( x (σi x)[shift]i).
Definition up_f `{funcs_signature} (σf : ar, function ar) ar := econs (@var_func _ 0 ar) ( x ar' (σf x ar')[shift ar]f).
Definition up_p `{preds_signature} (σp : ar, predicate ar) ar := econs (@var_pred _ 0 ar) ( x ar' (σp x ar')[shift ar]p).

#[global] Instance subst_form_i `{funcs_signature, preds_signature, operators} : Subst_i form := fix subst_form_i σi phi := match with
  | fal fal
  | atom P v atom P (Vector.map (subst_term_i σi) v)
  | bin op bin op (subst_form_i σi ) (subst_form_i σi )
  | quant_indi op quant_indi op (subst_form_i (up_i σi) )
  | quant_func op ar quant_func op ar (subst_form_i ( n (σi n)[shift ar]f ) )
  | quant_pred op ar quant_pred op ar (subst_form_i σi )
end.

#[global] Instance subst_form_f `{funcs_signature, preds_signature, operators} : Subst_f form := fix subst_form_f σf phi := match with
  | fal fal
  | atom P v atom P (Vector.map (subst_term_f σf) v)
  | bin op bin op (subst_form_f σf ) (subst_form_f σf )
  | quant_indi op quant_indi op (subst_form_f σf )
  | quant_func op ar quant_func op ar (subst_form_f (up_f σf ar) )
  | quant_pred op ar quant_pred op ar (subst_form_f σf )
end.

#[global] Instance subst_form_p `{funcs_signature, preds_signature, operators} : Subst_p form := fix subst_form_p σp phi := match with
  | fal fal
  | atom P v atom (subst_predicate σp P) v
  | bin op bin op (subst_form_p σp ) (subst_form_p σp )
  | quant_indi op quant_indi op (subst_form_p σp )
  | quant_func op ar quant_func op ar (subst_form_p σp )
  | quant_pred op ar quant_pred op ar (subst_form_p (up_p σp ar) )
end.

Declare Scope subst_scope.
Open Scope subst_scope.

Module SubstNotations.

  Notation "x .: sigma" := (econs x ) (at level 70, right associativity) : subst_scope.
  Notation "↑" := (shift) : subst_scope.
  Notation "f >> g" := ( x g (f x)) (at level 50) : subst_scope.
  Notation "f >>> g" := ( x y g (f x y)) (at level 50) : subst_scope.
  Notation "x '..'" := (econs x ids) (at level 1, format "x ..") : subst_scope.

  Notation "X [ σ ]i" := (subst_i σ X) (at level 7, left associativity, format "X '/' [ σ ]i").
  Notation "X [ σ ]f" := (subst_f σ X) (at level 7, left associativity, format "X '/' [ σ ]f").
  Notation "X [ σ ]p" := (subst_p σ X) (at level 7, left associativity, format "X '/' [ σ ]p").

End SubstNotations.

Section SubstLemmas.

  Import SubstNotations.

  Context {Σf2 : funcs_signature}.
  Context {Σp2 : preds_signature}.
  Context {ops : operators}.


  Lemma subst_term_ext_i sigma tau (t : term) :
    ( n, n = n) t[]i = t[]i.
  Proof.
    intros H. induction t; cbn. apply H. all: f_equal; apply map_ext_forall, IH.
  Qed.


  Lemma subst_term_ext_f sigma tau (t : term) :
    ( n ar, n ar = n ar) t[]f = t[]f.
  Proof.
    intros H. induction t; cbn.
    - reflexivity.
    - f_equal. apply H. apply map_ext_forall, IH.
    - f_equal. apply map_ext_forall, IH.
  Qed.


  Lemma subst_function_ext_f sigma tau ar (f : function ar) :
    ( n ar, n ar = n ar) f[]f = f[]f.
  Proof.
    intros H. destruct f; cbn. apply H. reflexivity.
  Qed.


  Lemma subst_predicate_ext_p sigma tau ar (P : predicate ar) :
    ( n ar, n ar = n ar) P[]p = P[]p.
  Proof.
    intros H. destruct P; cbn. apply H. reflexivity.
  Qed.


  Lemma subst_ext_i sigma tau (phi : form) :
    ( n, n = n) []i = []i.
  Proof.
    revert . induction ; intros H; cbn.
    - reflexivity.
    - f_equal. apply map_ext_forall, Forall_in. intros ? _. now apply subst_term_ext_i.
    - erewrite , . reflexivity. easy. easy.
    - erewrite IHphi. reflexivity. intros []; cbn. reflexivity. now rewrite H.
    - erewrite IHphi. reflexivity. intros n'. now rewrite H.
    - erewrite IHphi. reflexivity. easy.
  Qed.


  Lemma subst_ext_f sigma tau (phi : form) :
    ( n ar, n ar = n ar) []f = []f.
  Proof.
    revert . induction ; intros H; cbn.
    - reflexivity.
    - f_equal. apply map_ext_forall, Forall_in. intros ? _. now apply subst_term_ext_f.
    - erewrite , . reflexivity. easy. easy.
    - erewrite IHphi. reflexivity. easy.
    - erewrite IHphi. reflexivity. intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec as [|]; try easy; now rewrite H.
    - erewrite IHphi. reflexivity. easy.
  Qed.


  Lemma subst_ext_p sigma tau (phi : form) :
    ( n ar, n ar = n ar) []p = []p.
  Proof.
    revert . induction ; intros H; cbn.
    - reflexivity.
    - f_equal. now apply subst_predicate_ext_p.
    - erewrite , . reflexivity. easy. easy.
    - erewrite IHphi. reflexivity. easy.
    - erewrite IHphi. reflexivity. easy.
    - erewrite IHphi. reflexivity. intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec as [|]; try easy; now rewrite H.
  Qed.



  Let forall_map_eq X n (v : vec X n) p :
    Forall ( x p x = x) v Vector.map p v = v.
  Proof.
    intros H. induction v. reflexivity. cbn. f_equal. apply H. apply IHv, H.
  Qed.


  Lemma subst_term_id_i (t : term) :
    t[ids]i = t.
  Proof.
    induction t; cbn. reflexivity. unfold ids, var_func'. f_equal.
    apply forall_map_eq, IH. f_equal. apply forall_map_eq, IH.
  Qed.


  Lemma subst_term_id_f (t : SOL.term) :
    t[ids]f = t.
  Proof.
    induction t; cbn. reflexivity. unfold ids, var_func'. f_equal.
    apply forall_map_eq, IH. f_equal. apply forall_map_eq, IH.
  Qed.


  Lemma subst_id_i (phi : form) :
    [ids]i = .
  Proof.
    induction ; cbn; f_equal; try congruence.
    - apply forall_map_eq, Forall_in. intros ? _. apply subst_term_id_i.
    - rewrite IHphi at 2. apply subst_ext_i. now intros [].
    - rewrite IHphi at 2. apply subst_ext_i. now intros [].
  Qed.


  Lemma subst_id_f (phi : form) :
    [ids]f = .
  Proof.
    induction ; cbn; f_equal; try congruence.
    - apply forall_map_eq, Forall_in. intros ? _. apply subst_term_id_f.
    - rewrite IHphi at 2. apply subst_ext_f.
      intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec as [|]; cbn. reflexivity.
      all: unfold shift, shift_f; now destruct PeanoNat.Nat.eq_dec.
  Qed.


  Lemma subst_id_p (phi : form) :
    [ids]p = .
  Proof.
    induction ; cbn; f_equal; try congruence.
    - now destruct p.
    - rewrite IHphi at 2. apply subst_ext_p.
      intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec as [|]; cbn. reflexivity.
      all: unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
  Qed.



  Lemma subst_term_comp_i sigma tau (t : term) :
    t[]i[]i = t[ >> subst_term_i ]i.
  Proof.
    induction t; cbn. reflexivity. f_equal. rewrite Vector.map_map.
    apply map_ext_forall2, Forall2_identical, IH.
    f_equal. rewrite Vector.map_map. apply map_ext_forall, IH.
  Qed.


  Lemma subst_term_comp_f sigma tau (t : SOL.term) :
    t[]f[]f = t[ >>> subst_function ]f.
  Proof.
    induction t; cbn. reflexivity. f_equal. rewrite Vector.map_map.
    apply map_ext_forall, IH.
    f_equal. rewrite Vector.map_map. apply map_ext_forall, IH.
  Qed.


  Lemma up_funcomp_i sigma tau :
     n, (up_i >> subst_term_i (up_i )) n = up_i ( >> subst_term_i ) n.
  Proof.
    intros [|]; cbn; trivial. setoid_rewrite subst_term_comp_i.
    apply subst_term_ext_i. now intros [|].
  Qed.


  Lemma up_funcomp_f sigma tau ar :
     n ar', (up_f ar >>> subst_function (up_f ar)) n ar' = up_f ( >>> subst_function ) ar n ar'.
  Proof.
    intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [|]; unfold up_f; cbn.
      all: try unfold econs, econs_subst_func, econs_ar, shift, shift_f;
      try destruct PeanoNat.Nat.eq_dec as [|]; try easy; destruct ; try easy; cbn.
      + destruct PeanoNat.Nat.eq_dec; try easy; cbn. destruct ; cbn; now destruct PeanoNat.Nat.eq_dec.
      + repeat (destruct PeanoNat.Nat.eq_dec; try easy; cbn).
      + destruct PeanoNat.Nat.eq_dec; try easy; cbn. destruct ; cbn; now destruct PeanoNat.Nat.eq_dec.
  Qed.


  Lemma up_funcomp_p sigma tau ar :
     n ar', (up_p ar >>> subst_predicate (up_p ar)) n ar' = up_p ( >>> subst_predicate ) ar n ar'.
  Proof.
    intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [|]; unfold up_f; cbn.
      all: try unfold econs, econs_subst_func, econs_ar, shift, shift_p;
      try destruct PeanoNat.Nat.eq_dec as [|]; try easy; destruct ; try easy; cbn.
      + destruct PeanoNat.Nat.eq_dec; try easy; cbn. destruct ; cbn; now destruct PeanoNat.Nat.eq_dec.
      + repeat (destruct PeanoNat.Nat.eq_dec; try easy; cbn).
      + destruct PeanoNat.Nat.eq_dec; try easy; cbn. destruct ; cbn; now destruct PeanoNat.Nat.eq_dec.
  Qed.


  Lemma subst_term_swap_i_f tau sigma (t : term) :
    t[]i[]f = t[]f[ >> subst_f ]i.
  Proof.
    induction t; cbn.
    + reflexivity.
    + f_equal. rewrite !Vector.map_map. apply map_ext_forall, IH.
    + f_equal. rewrite !Vector.map_map. apply map_ext_forall, IH.
  Qed.


  Lemma subst_comp_i sigma tau (phi : form) :
    []i[]i = [ >> subst_term_i ]i.
  Proof.
    revert . induction ; intros ; cbn.
    - reflexivity.
    - f_equal. rewrite Vector.map_map. apply map_ext_forall, Forall_in.
      intros ? _. apply subst_term_comp_i.
    - now rewrite , .
    - f_equal. rewrite IHphi. apply subst_ext_i, up_funcomp_i.
    - f_equal. rewrite IHphi. apply subst_ext_i. intros n'; cbn.
      now setoid_rewrite subst_term_swap_i_f.
    - f_equal. now rewrite IHphi.
  Qed.


  Lemma subst_comp_f (phi : SOL.form) sigma tau :
    []f[]f = [ >>> subst_function ]f.
  Proof.
    revert . induction ; intros ; cbn.
    - reflexivity.
    - f_equal. rewrite Vector.map_map. apply map_ext_forall, Forall_in.
      intros ? _. apply subst_term_comp_f.
    - f_equal. now rewrite . now rewrite .
    - f_equal. now rewrite IHphi.
    - f_equal. rewrite IHphi. apply subst_ext_f, up_funcomp_f.
    - f_equal. now rewrite IHphi.
  Qed.


  Lemma subst_comp_p (phi : SOL.form) sigma tau :
    []p[]p = [ >>> subst_predicate ]p.
  Proof.
    revert . induction ; intros ; cbn.
    - reflexivity.
    - now destruct p.
    - f_equal. now rewrite . now rewrite .
    - f_equal. now rewrite IHphi.
    - f_equal. now rewrite IHphi.
    - f_equal. rewrite IHphi. apply subst_ext_p, up_funcomp_p.
  Qed.



  Lemma subst_term_switch_i_f (t : SOL.term) tau sigma :
    t[]i[]f = t[]f[ >> subst_f ]i.
  Proof.
    induction t; cbn.
    - reflexivity.
    - f_equal. rewrite !Vector.map_map. apply map_ext_forall, IH.
    - f_equal. rewrite !Vector.map_map. apply map_ext_forall, IH.
  Qed.


  Lemma subst_switch_i_f (phi : SOL.form) tau sigma :
    []i[]f = []f[ >> subst_f ]i.
  Proof.
    induction in , |- *; cbn.
    - reflexivity.
    - f_equal. rewrite !Vector.map_map. apply map_ext_in. intros ? _. apply subst_term_switch_i_f.
    - f_equal; firstorder.
    - f_equal. rewrite IHphi. apply subst_ext_i. intros []; cbn. reflexivity.
      symmetry. erewrite subst_term_ext_i. symmetry. apply subst_term_switch_i_f. reflexivity.
    - f_equal. rewrite IHphi. apply subst_ext_i. intros x. rewrite !subst_term_comp_f.
      apply subst_term_ext_f. intros [] ar; cbn; unfold shift, shift_f;
      now repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    - f_equal. apply IHphi.
  Qed.


  Lemma subst_switch_i_p (phi : SOL.form) tau sigma :
    []i[]p = []p[]i.
  Proof.
    induction in , |- *; cbn; f_equal; firstorder.
  Qed.


  Lemma subst_switch_f_p (phi : SOL.form) tau sigma :
    []f[]p = []p[]f.
  Proof.
    induction in , |- *; cbn; f_equal; firstorder.
  Qed.



  Lemma subst_term_ext_bounded_i n t sigma tau :
    bounded_indi_term n t ( x, x < n x = x) t[]i = t[]i.
  Proof.
    intros B H. induction t; cbn in *.
    - apply H. .
    - f_equal. eapply map_ext_forall, Forall_ext_Forall. apply IH. apply B.
    - f_equal. eapply map_ext_forall, Forall_ext_Forall. apply IH. apply B.
  Qed.


  Lemma subst_term_ext_bounded_f n ar t sigma tau :
    bounded_func_term ar n t ( x ar', ar ar' x < n x ar' = x ar') t[]f = t[]f.
  Proof.
    intros B H. induction t; cbn in *.
    - reflexivity.
    - f_equal. apply H. . eapply map_ext_forall, Forall_ext_Forall.
      apply IH. apply B.
    - f_equal. eapply map_ext_forall, Forall_ext_Forall. apply IH. apply B.
  Qed.


  Lemma subst_ext_bounded_i n phi sigma tau :
    bounded_indi n ( x, x < n x = x) []i = []i.
  Proof.
    induction in n, , |-*; cbn; intros B H.
    - reflexivity.
    - f_equal. apply map_ext_in. intros ? . eapply subst_term_ext_bounded_i.
      eapply Forall_in in B. apply B. easy. apply H.
    - now erewrite ( n), ( n).
    - erewrite (IHphi (S n)); try easy. intros [] ; cbn. reflexivity.
      rewrite H. reflexivity. .
    - erewrite (IHphi n); try easy. intros x . rewrite H. reflexivity. .
    - now erewrite (IHphi n).
  Qed.


  Lemma subst_ext_bounded_f n ar phi sigma tau :
    bounded_func ar n ( x ar', ar ar' x < n x ar' = x ar') []f = []f.
  Proof.
    induction in n, , |-*; cbn; intros B H.
    - reflexivity.
    - f_equal. apply map_ext_in. intros ? . eapply subst_term_ext_bounded_f.
      eapply Forall_in in B. apply B. easy. apply H.
    - now erewrite ( n), ( n).
    - now erewrite (IHphi n).
    - assert (ar = ar ) as [|] by .
      + destruct B as [[ B]|]; try . erewrite (IHphi (S n)); try easy.
        intros [] ar' ; cbn; destruct PeanoNat.Nat.eq_dec as [|]. reflexivity.
        all: rewrite H; try reflexivity; .
      + destruct B as [|[ B]]; try . erewrite (IHphi n); try easy.
        intros [] ar' ; cbn; destruct PeanoNat.Nat.eq_dec as [|]. reflexivity.
        all: rewrite H; try reflexivity; .
    - now erewrite (IHphi n).
  Qed.


  Lemma subst_ext_bounded_p n ar phi sigma tau :
    bounded_pred ar n ( x ar', ar ar' x < n x ar' = x ar') []p = []p.
  Proof.
    induction in n, , |-*; cbn; intros B H.
    - reflexivity.
    - destruct p; cbn. rewrite H. reflexivity. . reflexivity.
    - now erewrite ( n), ( n).
    - now erewrite (IHphi n).
    - now erewrite (IHphi n).
    - assert (ar = ar ) as [|] by .
      + destruct B as [[ B]|]; try . erewrite (IHphi (S n)); try easy.
        intros [] ar' ; cbn; destruct PeanoNat.Nat.eq_dec as [|]. reflexivity.
        all: rewrite H; try reflexivity; .
      + destruct B as [|[ B]]; try . erewrite (IHphi n); try easy.
        intros [] ar' ; cbn; destruct PeanoNat.Nat.eq_dec as [|]. reflexivity.
        all: rewrite H; try reflexivity; .
  Qed.


  Corollary subst_ext_i_closed phi sigma tau :
    bounded_indi 0 []i = []i.
  Proof.
    intros B. eapply subst_ext_bounded_i. apply B. .
  Qed.


  Corollary subst_ext_p_closed phi sigma tau ar :
    bounded_pred ar 0 ( ar', ar ar' x, x ar' = x ar') []p = []p.
  Proof.
    intros B H. eapply subst_ext_bounded_p. apply B. intros x ar' []. now apply H. .
  Qed.


  Lemma bounded_indi_subst_p n phi sigma :
    bounded_indi n bounded_indi n ([]p).
  Proof.
    revert n . induction ; firstorder.
  Qed.


  Lemma bounded_pred_subst_p ar b phi sigma :
    ( x, x ar = var_pred x) bounded_pred ar b bounded_pred ar b ([]p).
  Proof.
    revert b. induction ; intros b' Hsigma H; cbn.
    - easy.
    - destruct p; cbn. 2: easy. destruct (PeanoNat.Nat.eq_dec ar ) as [|].
      rewrite Hsigma. destruct H; . destruct ; .
    - firstorder.
    - firstorder.
    - firstorder.
    - destruct H.
      + left. split. easy. apply IHphi. 2: easy. intros []; unfold up_p, econs, shift, shift_p; cbn;
        destruct PeanoNat.Nat.eq_dec as [|]; try ; cbn. reflexivity. specialize (Hsigma ).
        destruct ; cbn. destruct PeanoNat.Nat.eq_dec; try easy. congruence. congruence.
      + right. split. easy. apply IHphi. 2: easy. intros x. specialize (Hsigma x).
        destruct x; unfold up_p, econs, shift, shift_p; cbn; destruct PeanoNat.Nat.eq_dec as [|]; try ;
        destruct ; cbn; try destruct PeanoNat.Nat.eq_dec; congruence.
  Qed.



  Lemma subst_term_shift_i (t : term) x :
    t[]i[x..]i = t.
  Proof.
    rewrite subst_term_comp_i. rewrite subst_term_id_i. now apply subst_term_ext_i.
  Qed.


  Lemma subst_form_shift_i (phi : form) x :
    []i[x..]i = .
  Proof.
    rewrite subst_comp_i. rewrite subst_id_i. now apply subst_ext_i.
  Qed.


  Lemma subst_term_shift_f (t : term) ar (f : function ar) :
    t[ ar]f[f..]f = t.
  Proof.
    rewrite subst_term_comp_f. rewrite subst_term_id_f. apply subst_term_ext_f.
    intros n ar'. unfold shift, shift_f. repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    reflexivity. now destruct n; cbn; destruct PeanoNat.Nat.eq_dec; try .
  Qed.


  Lemma subst_function_shift_f ar' (f : function ar') ar (x : function ar) :
    f[ ar]f[x..]f = f.
  Proof.
    destruct f; cbn. unfold shift, shift_f. now destruct n; repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    reflexivity.
  Qed.


  Lemma subst_form_shift_f (phi : form) ar (f : function ar) :
    [ ar]f[f..]f = .
  Proof.
    rewrite subst_comp_f. rewrite subst_id_f. apply subst_ext_f.
    intros n ar'. unfold shift, shift_f. repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    reflexivity. now destruct n; cbn; destruct PeanoNat.Nat.eq_dec; try .
  Qed.


  Lemma subst_predicate_shift_p ar' (P : predicate ar') ar (x : predicate ar) :
    P[ ar]p[x..]p = P.
  Proof.
    destruct P; cbn. unfold shift, shift_p. now destruct n; repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    reflexivity.
  Qed.


  Lemma subst_form_shift_p (phi : form) ar (P : predicate ar) :
    [ ar]p[P..]p = .
  Proof.
    rewrite subst_comp_p. rewrite subst_id_p. apply subst_ext_p.
    intros n ar'. unfold shift, shift_p. repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn).
    reflexivity. now destruct n; cbn; destruct PeanoNat.Nat.eq_dec; try .
  Qed.


  Lemma up_form_i phi sigma :
    []i[up_i ]i = []i[]i.
  Proof.
    rewrite !subst_comp_i. now apply subst_ext_i.
  Qed.


  Lemma up_form_f phi sigma ar :
    [ ar]f[up_f ar]f = []f[ ar]f.
  Proof.
    rewrite !subst_comp_f. apply subst_ext_f. intros n ar'. unfold shift, shift_f.
    repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn). now destruct .
    destruct n; cbn; now destruct PeanoNat.Nat.eq_dec.
  Qed.


  Lemma up_form_p phi sigma ar :
    [ ar]p[up_p ar]p = []p[ ar]p.
  Proof.
    rewrite !subst_comp_p. apply subst_ext_p. intros n ar'. unfold shift, shift_p.
    repeat (destruct PeanoNat.Nat.eq_dec; try ; cbn). now destruct .
    destruct n; cbn; now destruct PeanoNat.Nat.eq_dec.
  Qed.


  Lemma funcfreeTerm_subst_i t sigma :
    ( x, funcfreeTerm ( x)) funcfreeTerm t funcfreeTerm (t[]i).
  Proof.
    intros H F. induction t; cbn; trivial. eapply Forall_map, Forall_ext_Forall.
    apply IH. apply F.
  Qed.


  Lemma funcfreeTerm_subst_f t sigma :
    funcfreeTerm t funcfreeTerm (t[]f).
  Proof.
    intros F. induction t; cbn; trivial. now exfalso. eapply Forall_map, Forall_ext_Forall.
    apply IH. apply F.
  Qed.


  Lemma funcfree_subst_i phi sigma :
    ( x, funcfreeTerm ( x)) funcfree funcfree([]i).
  Proof.
    revert . induction ; intros H F; cbn. 1,3-6: firstorder.
    - apply IHphi; trivial. intros []; cbn. easy. now apply funcfreeTerm_subst_i.
    - apply Forall_map, Forall_in. intros v . apply funcfreeTerm_subst_i. easy.
      eapply Forall_in in F. apply F. easy.
  Qed.


  Lemma funcfree_subst_f phi sigma :
    funcfree funcfree([]f).
  Proof.
    induction in |-*; cbn; firstorder. apply Forall_in.
    intros v [? [ ?]]%vect_in_map_iff. apply funcfreeTerm_subst_f.
    eapply Forall_in in H. apply H. easy.
  Qed.


  Lemma funcfree_subst_p phi sigma :
    funcfree funcfree([]p).
  Proof.
    induction in |-*; firstorder.
  Qed.


End SubstLemmas.