From Coq Require Import Morphisms.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICInduction
  PCUICLiftSubst PCUICUnivSubst
  PCUICTyping PCUICEquality PCUICOnFreeVars
  PCUICSigmaCalculus PCUICRenameDef.

Require Import ssreflect ssrbool.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
Set Equations With UIP.
Set Keyed Unification.
Set Default Goal Selector "!".
Implicit Types cf : checker_flags.

Open Scope sigma_scope.

Definition inst_context σ (Γ : context) : context :=
  fold_context_k (fun i ⇒ inst (⇑^i σ)) Γ.

#[global] Instance inst_context_ext : Proper (`=1` ==> Logic.eq ==> Logic.eq) inst_context.
Proof.
  intros f g Hfg x y →.
  apply fold_context_k_ext ⇒ i t.
  now rewrite Hfg.
Qed.

Definition inst_decl σ d := map_decl (inst σ) d.

Definition inst_context_snoc0 s Γ d :
  inst_context s (d :: Γ) =
  inst_context s Γ ,, map_decl (inst (⇑^#|Γ| s)) d.
Proof. unfold inst_context. now rewrite fold_context_k_snoc0. Qed.
#[global] Hint Rewrite inst_context_snoc0 : sigma.

Definition inst_mutual_inductive_body σ m :=
  map_mutual_inductive_body (fun i ⇒ inst (⇑^i σ)) m.

Definition usubst (Γ : context) σ (Δ : context) :=
  ∀ x decl,
    nth_error Γ x = Some decl →
    (∀ b,
        decl.(decl_body) = Some b →
        (∑ x' decl', σ x = tRel x' ×
          nth_error Δ x' = Some decl' ×
          

          option_map (rename (rshiftk (S x'))) decl'.(decl_body) = Some (b.[↑^(S x) ∘s σ])) +
        
        (σ x = b.[↑^(S x) ∘s σ])).

Definition closed_subst (Γ : context) σ (Δ : context) :=
  is_closed_context Δ ×
  (∀ x decl, nth_error Γ x = Some decl → is_open_term Δ (σ x)) ×
  usubst Γ σ Δ.


Definition well_subst {cf} Σ (Γ : context) σ (Δ : context) :=
  (∀ x decl,
    nth_error Γ x = Some decl →
    Σ ;;; Δ |- σ x : ((lift0 (S x)) (decl_type decl)).[ σ ]) ×
  usubst Γ σ Δ.

Notation "Σ ;;; Δ ⊢ σ : Γ" :=
  (well_subst Σ Γ σ Δ) (at level 50, Δ, σ, Γ at next level).