Definition atom t :=
  match t with
  | tRel _
  | tVar _
  | tSort _
  | tConst _ _
  | tInd _ _
  | tConstruct _ _ _ ⇒ true
  | _ ⇒ false
  end.

Lemma red1_red (Σ : global_env) Γ t u : red1 Σ Γ t u → red Σ Γ t u.

Lemma red_step Σ Γ t u v : red1 Σ Γ t u → red Σ Γ u v → red Σ Γ t v.

Lemma red_alt@{i j +} Σ Γ t u : red Σ Γ t u <~> clos_refl_trans@{i j} (red1 Σ Γ) t u.

Lemma red_trans Σ Γ t u v : red Σ Γ t u → red Σ Γ u v → red Σ Γ t v.

Instance red_Transitive Σ Γ : Transitive (red Σ Γ).

Section ReductionCongruence.
  Context {Σ : global_env}.

  Inductive term_context : Set :=
  | tCtxHole : term_context
  | tCtxEvar : nat → list_context → term_context
  | tCtxProd_l : name → term_context → term → term_context
  | tCtxProd_r : name → term → term_context → term_context
  | tCtxLambda_l : name → term_context → term → term_context
  | tCtxLambda_r : name → term → term_context → term_context
  | tCtxLetIn_l : name → term_context → term →
                    term → term_context
  | tCtxLetIn_b : name → term → term_context →
                    term → term_context
  | tCtxLetIn_r : name → term → term →
                    term_context → term_context
  | tCtxApp_l : term_context → term → term_context
  | tCtxApp_r : term → term_context → term_context
  | tCtxCase_pred : (inductive × nat) → term_context
                         → term → list (nat × term) → term_context
  | tCtxCase_discr : (inductive × nat) → term
                 → term_context → list (nat × term) → term_context
  | tCtxCase_branch : (inductive × nat) → term
                           → term → list_nat_context → term_context
  | tCtxProj : projection → term_context → term_context
  
  

  with list_context : Set :=
   | tCtxHead : term_context → list term → list_context
   | tCtxTail : term → list_context → list_context

  with list_nat_context : Set :=
   | tCtxHead_nat : (nat × term_context) → list (nat × term) → list_nat_context
   | tCtxTail_nat : (nat × term) → list_nat_context → list_nat_context.



  Section FillContext.
    Context (t : term).

    Equations fill_context (ctx : term_context) : term by struct ctx := {
    | tCtxHole ⇒ t;
    | tCtxEvar n l ⇒ tEvar n (fill_list_context l);
    | tCtxProd_l na ctx b ⇒ tProd na (fill_context ctx) b;
    | tCtxProd_r na ty ctx ⇒ tProd na ty (fill_context ctx);
    | tCtxLambda_l na ty b ⇒ tLambda na (fill_context ty) b;
    | tCtxLambda_r na ty b ⇒ tLambda na ty (fill_context b);
    | tCtxLetIn_l na b ty b' ⇒ tLetIn na (fill_context b) ty b';
    | tCtxLetIn_b na b ty b' ⇒ tLetIn na b (fill_context ty) b';
    | tCtxLetIn_r na b ty b' ⇒ tLetIn na b ty (fill_context b');
    | tCtxApp_l f a ⇒ tApp (fill_context f) a;
    | tCtxApp_r f a ⇒ tApp f (fill_context a);
    | tCtxCase_pred par p c brs ⇒ tCase par (fill_context p) c brs;
    | tCtxCase_discr par p c brs ⇒ tCase par p (fill_context c) brs;
    | tCtxCase_branch par p c brs ⇒ tCase par p c (fill_list_nat_context brs);
    | tCtxProj p c ⇒ tProj p (fill_context c) }
    
    

    with fill_list_context (l : list_context) : list term by struct l :=
    { fill_list_context (tCtxHead ctx l) ⇒ (fill_context ctx) :: l;
      fill_list_context (tCtxTail hd ctx) ⇒ hd :: fill_list_context ctx }

    with fill_list_nat_context (l : list_nat_context) : list (nat × term) by struct l :=
    { fill_list_nat_context (tCtxHead_nat (n, ctx) l) ⇒ (n, fill_context ctx) :: l;
      fill_list_nat_context (tCtxTail_nat hd ctx) ⇒ hd :: fill_list_nat_context ctx }.


    Equations hole_context (ctx : term_context) (Γ : context) : context by struct ctx := {
    | tCtxHole | Γ ⇒ Γ;
    | tCtxEvar n l | Γ ⇒ hole_list_context l Γ;
    | tCtxProd_l na ctx b | Γ ⇒ hole_context ctx Γ;
    | tCtxProd_r na ty ctx | Γ ⇒ hole_context ctx (Γ ,, vass na ty);
    | tCtxLambda_l na ty b | Γ ⇒ hole_context ty Γ;
    | tCtxLambda_r na ty b | Γ ⇒ hole_context b (Γ ,, vass na ty);
    | tCtxLetIn_l na b ty b' | Γ ⇒ hole_context b Γ;
    | tCtxLetIn_b na b ty b' | Γ ⇒ hole_context ty Γ;
    | tCtxLetIn_r na b ty b' | Γ ⇒ hole_context b' (Γ ,, vdef na b ty);
    | tCtxApp_l f a | Γ ⇒ hole_context f Γ;
    | tCtxApp_r f a | Γ ⇒ hole_context a Γ;
    | tCtxCase_pred par p c brs | Γ ⇒ hole_context p Γ;
    | tCtxCase_discr par p c brs | Γ ⇒ hole_context c Γ;
    | tCtxCase_branch par p c brs | Γ ⇒ hole_list_nat_context brs Γ;
    | tCtxProj p c | Γ ⇒ hole_context c Γ }
    
    

    with hole_list_context (l : list_context) (Γ : context) : context by struct l :=
    { hole_list_context (tCtxHead ctx l) Γ ⇒ hole_context ctx Γ;
      hole_list_context (tCtxTail hd ctx) Γ ⇒ hole_list_context ctx Γ }

    with hole_list_nat_context (l : list_nat_context) (Γ : context) : context by struct l :=
    { hole_list_nat_context (tCtxHead_nat (n, ctx) l) Γ ⇒ hole_context ctx Γ;
      hole_list_nat_context (tCtxTail_nat hd ctx) Γ ⇒ hole_list_nat_context ctx Γ }.


  End FillContext.

  Inductive contextual_closure (red : ∀ Γ, term → term → Type) : context → term → term → Type :=
  | ctxclos_atom Γ t : atom t → contextual_closure red Γ t t
  | ctxclos_ctx Γ (ctx : term_context) (u u' : term) :
      red (hole_context ctx Γ) u u' → contextual_closure red Γ (fill_context u ctx) (fill_context u' ctx).

  Lemma red_contextual_closure Γ t u : red Σ Γ t u → contextual_closure (red Σ) Γ t u.


  Lemma contextual_closure_red Γ t u : contextual_closure (red Σ) Γ t u → red Σ Γ t u.

  Theorem red_contextual_closure_equiv Γ t u : red Σ Γ t u <~> contextual_closure (red Σ) Γ t u.


  Lemma red_ctx {Γ} {M M'} ctx : red Σ (hole_context ctx Γ) M M' →
                               red Σ Γ (fill_context M ctx) (fill_context M' ctx).

  Section Congruences.

    Inductive redl Γ {A} l : list (term × A) → Type :=
    | refl_redl : redl Γ l l
    | trans_redl :
        ∀ l1 l2,
          redl Γ l l1 →
          OnOne2 (Trel_conj (on_Trel (red1 Σ Γ) fst) (on_Trel eq snd)) l1 l2 →
          redl Γ l l2.

    Lemma OnOne2_red_redl :
      ∀ Γ A (l l' : list (term × A)),
        OnOne2 (Trel_conj (on_Trel (red Σ Γ) fst) (on_Trel eq snd)) l l' →
        redl Γ l l'.

    Lemma OnOne2_on_Trel_eq_red_redl :
      ∀ Γ A B (f : A → term) (g : A → B) l l',
        OnOne2 (on_Trel_eq (red Σ Γ) f g) l l' →
        redl Γ (map (fun x ⇒ (f x, g x)) l) (map (fun x ⇒ (f x, g x)) l').

    Lemma OnOne2_prod_inv :
      ∀ A (P : A → A → Type) Q l l',
        OnOne2 (Trel_conj P Q) l l' →
        OnOne2 P l l' × OnOne2 Q l l'.

    Lemma OnOne2_prod_inv_refl_r :
      ∀ A (P Q : A → A → Type) l l',
        (∀ x, Q x x) →
        OnOne2 (Trel_conj P Q) l l' →
        OnOne2 P l l' × All2 Q l l'.

    Lemma All2_eq :
      ∀ A (l l' : list A),
        All2 eq l l' →
        l = l'.

    Lemma list_split_eq :
      ∀ A B (l l' : list (A × B)),
        map fst l = map fst l' →
        map snd l = map snd l' →
        l = l'.

    Notation swap := (fun x ⇒ (snd x, fst x)).

    Lemma list_map_swap_eq :
      ∀ A B (l l' : list (A × B)),
        map swap l = map swap l' →
        l = l'.

    Lemma map_swap_invol :
      ∀ A B (l : list (A × B)),
        l = map swap (map swap l).

    Lemma map_inj :
      ∀ A B (f : A → B) l l',
        (∀ x y, f x = f y → x = y) →
        map f l = map f l' →
        l = l'.

    Context {Γ : context}.

    Lemma red_abs na M M' N N' : red Σ Γ M M' → red Σ (Γ ,, vass na M') N N' →
                                               red Σ Γ (tLambda na M N) (tLambda na M' N').

    Lemma red_app M0 M1 N0 N1 :
      red Σ Γ M0 M1 →
      red Σ Γ N0 N1 →
      red Σ Γ (tApp M0 N0) (tApp M1 N1).

    Fixpoint mkApps_context l :=
      match l with
      | [] ⇒ tCtxHole
      | hd :: tl ⇒ tCtxApp_l (mkApps_context tl) hd
      end.

    Lemma mkApps_context_hole l Γ' : hole_context (mkApps_context (List.rev l)) Γ' = Γ'.

    Lemma fill_mkApps_context M l : fill_context M (mkApps_context (List.rev l)) = mkApps M l.

    Lemma red1_mkApps_f :
      ∀ t u l,
        red1 Σ Γ t u →
        red1 Σ Γ (mkApps t l) (mkApps u l).

    Corollary red_mkApps_f :
      ∀ t u l,
        red Σ Γ t u →
        red Σ Γ (mkApps t l) (mkApps u l).

    Lemma red_mkApps M0 M1 N0 N1 :
      red Σ Γ M0 M1 →
      All2 (red Σ Γ) N0 N1 →
      red Σ Γ (mkApps M0 N0) (mkApps M1 N1).

    Lemma red_letin na d0 d1 t0 t1 b0 b1 :
      red Σ Γ d0 d1 → red Σ Γ t0 t1 → red Σ (Γ ,, vdef na d1 t1) b0 b1 →
      red Σ Γ (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1).

    Lemma red_case_p :
      ∀ indn p c brs p',
        red Σ Γ p p' →
        red Σ Γ (tCase indn p c brs) (tCase indn p' c brs).

    Lemma red_case_c :
      ∀ indn p c brs c',
        red Σ Γ c c' →
        red Σ Γ (tCase indn p c brs) (tCase indn p c' brs).

    Lemma red_case_one_brs :
      ∀ indn p c brs brs',
        OnOne2 (on_Trel_eq (red Σ Γ) snd fst) brs brs' →
        red Σ Γ (tCase indn p c brs) (tCase indn p c brs').

    Inductive rtrans_clos {A} (R : A → A → Type) (x : A) : A → Type :=
    | rtrans_clos_refl : rtrans_clos R x x
    | rtrans_clos_trans :
        ∀ y z,
          rtrans_clos R x y →
          R y z →
          rtrans_clos R x z.

    Lemma All2_many_OnOne2 :
      ∀ A (R : A → A → Type) l l',
        All2 R l l' →
        rtrans_clos (OnOne2 R) l l'.

    Lemma red_case_brs :
      ∀ indn p c brs brs',
        All2 (on_Trel_eq (red Σ Γ) snd fst) brs brs' →
        red Σ Γ (tCase indn p c brs) (tCase indn p c brs').


    Lemma All2_ind_OnOne2 {A} P (l l' : list A) :
      All2 P l l' →
      ∀ x a a', nth_error l x = Some a →
                     nth_error l' x = Some a' →
                     OnOne2 P (firstn x l ++ [a] ++ skipn (S x) l)%list
                            (firstn x l ++ [a'] ++ skipn (S x) l)%list.

    Lemma reds_case :
      ∀ indn p c brs p' c' brs',
        red Σ Γ p p' →
        red Σ Γ c c' →
        All2 (on_Trel_eq (red Σ Γ) snd fst) brs brs' →
        red Σ Γ (tCase indn p c brs) (tCase indn p' c' brs').

    Lemma red1_it_mkLambda_or_LetIn :
      ∀ Δ u v,
        red1 Σ (Γ ,,, Δ) u v →
        red1 Σ Γ (it_mkLambda_or_LetIn Δ u)
             (it_mkLambda_or_LetIn Δ v).

    Lemma red_it_mkLambda_or_LetIn :
      ∀ Δ u v,
        red Σ (Γ ,,, Δ) u v →
        red Σ Γ (it_mkLambda_or_LetIn Δ u)
            (it_mkLambda_or_LetIn Δ v).

    Lemma red_proj_c :
      ∀ p c c',
        red Σ Γ c c' →
        red Σ Γ (tProj p c) (tProj p c').

    Lemma red_fix_one_ty :
      ∀ mfix idx mfix',
        OnOne2 (on_Trel_eq (red Σ Γ) dtype (fun x ⇒ (dname x, dbody x, rarg x))) mfix mfix' →
        red Σ Γ (tFix mfix idx) (tFix mfix' idx).

    Lemma red_fix_ty :
      ∀ mfix idx mfix',
        All2 (on_Trel_eq (red Σ Γ) dtype (fun x ⇒ (dname x, dbody x, rarg x))) mfix mfix' →
        red Σ Γ (tFix mfix idx) (tFix mfix' idx).

    Lemma red_fix_one_body :
      ∀ mfix idx mfix',
        OnOne2
          (on_Trel_eq (red Σ (Γ ,,, fix_context mfix)) dbody (fun x ⇒ (dname x, dtype x, rarg x)))
           mfix mfix' →
        red Σ Γ (tFix mfix idx) (tFix mfix' idx).

    Lemma red_fix_body :
      ∀ mfix idx mfix',
        All2
          (on_Trel_eq (red Σ (Γ ,,, fix_context mfix)) dbody (fun x ⇒ (dname x, dtype x, rarg x)))
           mfix mfix' →
        red Σ Γ (tFix mfix idx) (tFix mfix' idx).

    Lemma red_fix_congr :
      ∀ mfix mfix' idx,
        All2 (fun d0 d1 ⇒
                (red Σ Γ (dtype d0) (dtype d1)) ×
                (red Σ (Γ ,,, fix_context mfix) (dbody d0) (dbody d1) ×
                (dname d0, rarg d0) = (dname d1, rarg d1))
        ) mfix mfix' →
      red Σ Γ (tFix mfix idx) (tFix mfix' idx).

    Lemma red_cofix_one_ty :
      ∀ mfix idx mfix',
        OnOne2 (on_Trel_eq (red Σ Γ) dtype (fun x ⇒ (dname x, dbody x, rarg x))) mfix mfix' →
        red Σ Γ (tCoFix mfix idx) (tCoFix mfix' idx).

    Lemma red_cofix_ty :
      ∀ mfix idx mfix',
        All2 (on_Trel_eq (red Σ Γ) dtype (fun x ⇒ (dname x, dbody x, rarg x))) mfix mfix' →
        red Σ Γ (tCoFix mfix idx) (tCoFix mfix' idx).

    Lemma red_cofix_one_body :
      ∀ mfix idx mfix',
        OnOne2
          (on_Trel_eq (red Σ (Γ ,,, fix_context mfix)) dbody (fun x ⇒ (dname x, dtype x, rarg x)))
           mfix mfix' →
        red Σ Γ (tCoFix mfix idx) (tCoFix mfix' idx).

    Lemma red_cofix_body :
      ∀ mfix idx mfix',
        All2
          (on_Trel_eq (red Σ (Γ ,,, fix_context mfix)) dbody (fun x ⇒ (dname x, dtype x, rarg x)))
           mfix mfix' →
        red Σ Γ (tCoFix mfix idx) (tCoFix mfix' idx).

    Lemma red_cofix_congr :
      ∀ mfix mfix' idx,
        All2 (fun d0 d1 ⇒
                (red Σ Γ (dtype d0) (dtype d1)) ×
                (red Σ (Γ ,,, fix_context mfix) (dbody d0) (dbody d1) ×
                (dname d0, rarg d0) = (dname d1, rarg d1))
        ) mfix mfix' →
      red Σ Γ (tCoFix mfix idx) (tCoFix mfix' idx).

    Lemma red_prod_l :
      ∀ na A B A',
        red Σ Γ A A' →
        red Σ Γ (tProd na A B) (tProd na A' B).

    Lemma red_prod_r :
      ∀ na A B B',
        red Σ (Γ ,, vass na A) B B' →
        red Σ Γ (tProd na A B) (tProd na A B').

    Lemma red_prod :
      ∀ na A B A' B',
        red Σ Γ A A' →
        red Σ (Γ ,, vass na A) B B' →
        red Σ Γ (tProd na A B) (tProd na A' B').

    Lemma OnOne2_on_Trel_eq_unit :
      ∀ A (R : A → A → Type) l l',
        OnOne2 R l l' →
        OnOne2 (on_Trel_eq R (fun x ⇒ x) (fun x ⇒ tt)) l l'.

    Lemma red_one_evar :
      ∀ ev l l',
        OnOne2 (red Σ Γ) l l' →
        red Σ Γ (tEvar ev l) (tEvar ev l').

    Lemma red_evar :
      ∀ ev l l',
        All2 (red Σ Γ) l l' →
        red Σ Γ (tEvar ev l) (tEvar ev l').

    Lemma red_atom t : atom t → red Σ Γ t t.

  End Congruences.
End ReductionCongruence.



Lemma OnOne2_All2 {A}:
  ∀ (ts ts' : list A) P Q,
    OnOne2 P ts ts' →
    (∀ x y, P x y → Q x y)%type →
    (∀ x, Q x x) →
    All2 Q ts ts'.