gistfile1.coq

Require Import
  Coq.Relations.Relations Coq.Relations.Relation_Operators
  Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype
  Ssreflect.ssrnat Ssreflect.seq Omega.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Definition natE :=
  (addSn, addnS, add0n, addn0, sub0n, subn0, subSS,
   min0n, minn0, max0n, maxn0, leq0n).

CoInductive leq_xor_gtn' m n :
    bool -> bool -> bool -> bool ->
    nat -> nat -> nat -> nat -> nat -> nat -> Set :=
  | LeqNotGtn' of m <= n :
    leq_xor_gtn' m n (m < n) false true (n <= m) n n m m 0 (n - m)
  | GtnNotLeq' of n < m :
    leq_xor_gtn' m n false true false true m m n n (m - n) 0.

Lemma leqP' m n : leq_xor_gtn' m n
  (m < n) (n < m) (m <= n) (n <= m)
  (maxn m n) (maxn n m) (minn m n) (minn n m)
  (m - n) (n - m).
Proof.
  case: (leqP m n) => H; rewrite (maxnC n) (minnC n).
  - rewrite (maxn_idPr H) (minn_idPl H).
    by move: (H); rewrite -subn_eq0 => /eqP ->; constructor.
  - rewrite (ltnW H) ltnNge leq_eqVlt H orbT
            (maxn_idPl (ltnW H)) (minn_idPr (ltnW H)).
    by move: (ltnW H); rewrite -subn_eq0 => /eqP ->; constructor.
Qed.

Module simpl_natarith.
Lemma lem1_1 ml mr n r : ml = r + n -> ml + mr = r + mr + n.
Proof. by move => ->; rewrite addnAC. Qed.
Lemma lem1_2 ml mr n r : mr = r + n -> ml + mr = ml + r + n.
Proof. by move => ->; rewrite addnA. Qed.
Lemma lem1_3 m' n r : m' = r + n -> m'.+1 = r.+1 + n.
Proof. by move => ->; rewrite addSn. Qed.
Lemma lem2_1 ml mr n r : ml - n = r -> ml - mr - n = r - mr.
Proof. by move => <-; rewrite subnAC. Qed.
Lemma lem2_2 m' n r : m' - n = r -> m'.-1 - n = r.-1.
Proof. by move => <-; rewrite -subnS -add1n subnDA subn1. Qed.
Lemma lem2_3 m n r : m = r + n -> m - n = r.
Proof. by move => ->; rewrite addnK. Qed.
Lemma lem3_1 m m' m'' nl nl' nl'' nr nr' :
  m - nl = m' - nl' -> m' - nl' - nr = m'' - nl'' - nr' ->
  m - (nl + nr) = m'' - (nl'' + nr').
Proof. by rewrite !subnDA => -> ->. Qed.
Lemma lem3_2 m n r : m - (n + 1) = r -> m - n.+1 = r.
Proof. by rewrite addn1. Qed.
Lemma lem3_3 m n r : m - n = r -> m - n = r - 0.
Proof. by rewrite subn0. Qed.
Lemma lem4_1 m n m' n' : m - n = m' - n' -> (m <= n) = (m' <= n').
Proof. by rewrite -!subn_eq0 => ->. Qed.
End simpl_natarith.
Import simpl_natarith.

Ltac simpl_natarith1 m n :=
  match m with
    | n => constr: (esym (add0n n))
    | ?ml + ?mr => let H := simpl_natarith1 ml n in constr: (lem1_1 mr H)
    | ?ml + ?mr => let H := simpl_natarith1 mr n in constr: (lem1_2 ml H)
    | ?m'.+1 => let H := simpl_natarith1 m' n in constr: (lem1_3 H)
    | ?m'.+1 => match n with 1 => constr: (esym (addn1 m')) end
  end.

Ltac simpl_natarith2 m n :=
  match m with
    | ?ml - ?mr => let H := simpl_natarith2 ml n in constr: (lem2_1 mr H)
    | ?m'.-1 => let H := simpl_natarith2 m' n in constr: (lem2_2 H)
    | _ => let H := simpl_natarith1 m n in constr: (lem2_3 H)
  end.

Ltac simpl_natarith3 m n :=
  lazymatch n with
    | ?nl + ?nr =>
      simpl_natarith3 m nl;
      match goal with |- _ = ?m1 -> _ =>
        let H := fresh "H" in
        move => H; simpl_natarith3 m1 nr; move/(lem3_1 H) => {H}
      end
    | _ =>
      match n with
        | ?n'.+1 =>
          lazymatch n' with
            | 0 => fail
            | _ => simpl_natarith3 m (n' + 1); move/lem3_2
          end
        | _ => let H := simpl_natarith2 m n in move: (lem3_3 H)
        | _ => move: (erefl (m - n))
      end
  end.

Ltac simpl_natarith :=
  let tac :=
    lazymatch goal with
      | |- ?x = ?x -> _ => move => _; rewrite !natE
      | _ => move => ->; rewrite ?natE
    end in
  repeat match goal with
    | H : context [?m - ?n] |- _ => move: H; simpl_natarith3 m n; tac => H
    | |- context [?m - ?n] => simpl_natarith3 m n; tac
    | H : context [?m <= ?n] |- _ =>
      move: H; simpl_natarith3 m n; move/lem4_1; tac => H
    | |- context [?m <= ?n] => simpl_natarith3 m n; move/lem4_1; tac
  end;
  try done;
  repeat match goal with
    | H : is_true true |- _ => move => {H}
  end.

Tactic Notation "elimleq" :=
  match goal with
    | |- is_true (_ <= _ _) -> _ => fail
    | |- is_true (?m <= ?n) -> _ =>
      (let H := fresh "H" in move/subnKC => H; rewrite <- H in *; clear H);
      (let rec tac :=
        lazymatch reverse goal with
          | H : context [n] |- _ => move: H; tac => H
          | _ => move: {n} (n - m) => n; rewrite ?(addKn, addnK)
        end in tac);
      simpl_natarith
  end.

Tactic Notation "elimleq" constr(H) := move: H; elimleq.

Tactic Notation "find_minneq_hyp" constr(m) constr(n) :=
  match goal with
    | H : is_true (m <= n) |- _ => rewrite (minn_idPl H)
    | H : is_true (n <= m) |- _ => rewrite (minn_idPr H)
    | H : is_true (m < n) |- _ => rewrite (minn_idPl (ltnW H))
    | H : is_true (n < m) |- _ => rewrite (minn_idPr (ltnW H))
    | |- _ => case (leqP' m n)
  end; rewrite ?natE.

Tactic Notation "find_maxneq_hyp" constr(m) constr(n) :=
  match goal with
    | H : is_true (m <= n) |- _ => rewrite (maxn_idPr H)
    | H : is_true (n <= m) |- _ => rewrite (maxn_idPl H)
    | H : is_true (m < n) |- _ => rewrite (maxn_idPr (ltnW H))
    | H : is_true (n < m) |- _ => rewrite (maxn_idPl (ltnW H))
    | |- _ => case (leqP' m n)
  end; rewrite ?natE.

Ltac replace_minn_maxn :=
  try (rewrite <- minnE in * || rewrite <- maxnE in * );
  match goal with
    | H : context [minn ?m ?n] |- _ => move: H; find_minneq_hyp n m => H
    | H : context [maxn ?m ?n] |- _ => move: H; find_maxneq_hyp n m => H
    | |- context [minn ?m ?n] => find_minneq_hyp m n
    | |- context [maxn ?m ?n] => find_maxneq_hyp m n
  end;
  try (let x := fresh "x" in move => x).

Ltac arith_hypo_ssrnat2coqnat :=
  match goal with
    | H : is_true false    |- _ => by move: H
    | H : is_true (_ && _) |- _ => let H0 := fresh "H" in case/andP: H => H H0
    | H : is_true (_ || _) |- _ => case/orP in H
    | H : context [_ <  _] |- _ => move/ltP in H
    | H : context [_ <= _] |- _ => move/leP in H
    | H : context [_ == _] |- _ => move/eqP in H
  end.

Ltac arith_goal_ssrnat2coqnat :=
  match goal with
    | |- is_true (_ && _) => apply/andP; split
    | |- is_true (_ || _) => apply/orP
    | |- is_true (_ <  _) => apply/ltP
    | |- is_true (_ <= _) => apply/leP
    | |- is_true (_ == _) => apply/eqP
  end.

Ltac ssromega :=
  repeat (let x := fresh "x" in move => x);
  do ?replace_minn_maxn;
  try done;
  repeat match goal with H : is_true (?m <= ?n) |- _ => elimleq H end;
  do ?unfold addn, subn, muln, addn_rec, subn_rec, muln_rec in *;
  do ?arith_hypo_ssrnat2coqnat;
  do ?arith_goal_ssrnat2coqnat;
  omega.

Ltac elimif :=
  (match goal with
     | |- context [if ?m < ?n then _ else _] => case (leqP' n m)
     | |- context [if ?m <= ?n then _ else _] => case (leqP' m n)
     | |- context [if ?b then _ else _] => case (ifP b)
   end;
   move => //=; elimif; let hyp := fresh "H" in move => hyp) ||
  idtac.

Ltac elimif_omega :=
  elimif; simpl_natarith;
  repeat match goal with H : is_true (?m <= ?n) |- _ => elimleq H end;
  try (repeat match goal with
    | |- _ + _ = _ => idtac
    | |- _ - _ = _ => idtac
    | |- _ => f_equal
  end; ssromega).

Section Seq.

Variable (A B : Type).

Lemma drop_addn n m (xs : seq A) : drop n (drop m xs) = drop (n + m) xs.
Proof.
  elim: m xs => [| m IH] [] // x xs.
  - by rewrite addn0.
  - by rewrite addnS /= IH.
Qed.

Lemma size_take n (xs : seq A) : size (take n xs) = minn n (size xs).
Proof.
  elim: n xs => [xs | n IH [] //= _ xs].
  - by rewrite take0 min0n.
  - by rewrite minnSS IH.
Qed.

Lemma nth_map' (f : A -> B) x xs n : f (nth x xs n) = nth (f x) (map f xs) n.
Proof. by elim: xs n => [n | x' xs IH []] //=; rewrite !nth_nil. Qed.

Lemma nth_equal (a b : A) xs n :
  (size xs <= n -> a = b) -> nth a xs n = nth b xs n.
Proof. by elim: xs n => [n /= -> | x xs IH []]. Qed.

End Seq.

Definition insert A xs ys d n : seq A :=
  take n ys ++ nseq (n - size ys) d ++ xs ++ drop n ys.

Section Insert.

Variable (A B : Type).

Lemma size_insert (xs ys : seq A) d n :
  size (insert xs ys d n) = size xs + maxn n (size ys).
Proof. rewrite /insert !size_cat size_nseq size_take size_drop; ssromega. Qed.

Lemma map_insert (f : A -> B) xs ys d n :
  map f (insert xs ys d n) = insert (map f xs) (map f ys) (f d) n.
Proof. by rewrite /insert !map_cat map_take map_nseq size_map map_drop. Qed.

Lemma nth_insert (xs ys : seq A) d d' n m :
  nth d (insert xs ys d' n) m =
  if m < n then nth d' ys m else
  if m < n + size xs then nth d' xs (m - n) else nth d ys (m - size xs).
Proof.
  rewrite /insert !nth_cat size_take size_nseq -subnDA nth_drop.
  have ->: minn n (size ys) + (n - size ys) = n by ssromega.
  elimif; try ssromega.
  - apply nth_equal; ssromega.
  - rewrite nth_nseq H0 nth_default //; ssromega.
  - rewrite nth_take //; apply nth_equal; ssromega.
Qed.

Lemma take_insert n (xs ys : seq A) d :
  take n (insert xs ys d n) = take n ys ++ nseq (n - size ys) d.
Proof.
  by rewrite /insert take_cat size_take ltnNge geq_minl /= minnE subKn
             ?leq_subr // take_cat size_nseq ltnn subnn take0 cats0.
Qed.

Lemma drop_insert n (xs ys : seq A) d :
  drop (n + size xs) (insert xs ys d n) = drop n ys.
Proof.
  rewrite /insert !catA drop_cat !size_cat size_take size_nseq drop_addn.
  elimif_omega.
Qed.

End Insert.

Definition context A := (seq (option A)).

Notation ctxindex xs n x := (Some x == nth None xs n).
Notation ctxmap f xs := (map (omap f) xs).
Notation ctxinsert xs ys n := (insert xs ys None n).

Section Context.

Variable (A : eqType).

Fixpoint ctxleq_rec (xs ys : context A) : bool :=
  match xs, ys with
    | [::], _ => true
    | (None :: xs), [::] => ctxleq_rec xs [::]
    | (None :: xs), (_ :: ys) => ctxleq_rec xs ys
    | (Some _ :: _), [::] => false
    | (Some x :: xs), (Some y :: ys) => (x == y) && ctxleq_rec xs ys
    | (Some _ :: _), (None :: _) => false
  end.

Definition ctxleq := nosimpl ctxleq_rec.

Infix "<=c" := ctxleq (at level 70, no associativity).

Lemma ctxleqE xs ys :
  (xs <=c ys) =
  ((head None xs == head None ys) || (head None xs == None)) &&
    (behead xs <=c behead ys).
Proof.
  move: xs ys => [| [x |] xs] [| [y |] ys] //=.
  by case/boolP: (Some x == None) => // _; rewrite orbF.
Qed.

Lemma ctxleqP (xs ys : context A) :
  reflect (forall n a, ctxindex xs n a -> ctxindex ys n a) (ctxleq xs ys).
Proof.
  apply: (iffP idP); elim: xs ys => [| x xs IH] //.
  - by move => ys _ n a; rewrite nth_nil.
  - by case => [| y ys]; rewrite ctxleqE /= =>
      /andP [] /orP [] /eqP -> H [] //= n a /(IH _ H) //; rewrite nth_nil.
  - by case => [| y ys]; rewrite ctxleqE /= => H; apply/andP;
      (apply conj;
       [ case: x H; rewrite ?eqxx ?orbT // => x H; rewrite (H 0 x) |
         apply IH => n a /(H n.+1 a) ]).
Qed.

End Context.

Infix "<=c" := ctxleq (at level 70, no associativity).

Lemma ctxleq_map (A B : eqType) (f : A -> B) xs ys :
  xs <=c ys -> ctxmap f xs <=c ctxmap f ys.
Proof.
  move/ctxleqP => H; apply/ctxleqP => n a.
  move: (H n); rewrite -!(nth_map' (omap f) None).
  by case: (nth None xs n) => //= a' /(_ a' (eqxx _)) /eqP => <-.
Qed.

Fixpoint Forall A (P : A -> Prop) xs :=
  if xs is x :: xs then P x /\ Forall P xs else True.

Notation inclusion R R' := (forall t1 t2, R t1 t2 -> R' t1 t2).

Notation "[ * R ]" :=
  (clos_refl_trans_1n _ R) (at level 5, no associativity) : type_scope.

Hint Resolve rt1n_refl.

Lemma rtc_trans' A R : Relation_Definitions.transitive A [* R].
Proof.
  move => t1 t2 t3.
  rewrite -!clos_rt_rt1n_iff.
  apply rt_trans.
Qed.

Lemma rtc_step A (R : relation A) : inclusion R [* R].
Proof. by move => x y H; apply rt1n_trans with y. Qed.

Lemma rtc_map' A B (R : relation A) (R' : relation B) (f : A -> B) :
  inclusion R (fun x y => R' (f x) (f y)) ->
  inclusion [* R] (fun x y => [* R'] (f x) (f y)).
Proof.
  move => H.
  refine (clos_refl_trans_1n_ind A R _ _ _) => //= x y z H0 H1 H2.
  apply rt1n_trans with (f y); auto.
Qed.

Lemma acc_preservation A B (RA : relation A) (RB : relation B) (f : A -> B) a :
  (forall x y, RA x y -> RB (f x) (f y)) -> Acc RB (f a) -> Acc RA a.
Proof.
  move => H H0; move: {1 2}(f a) H0 (erefl (f a)) => b H0; move: b H0 a.
  refine (Acc_ind _ _) => b _ H0 a H1; subst b.
  by constructor => a' H1; apply (fun x => H0 _ x _ erefl), H.
Qed.

Inductive typ := tyvar of nat | tyfun of typ & typ | tyabs of typ.

Inductive term
  := var  of nat                       (* variable *)
   | app  of term & term & typ         (* value application *)
   | abs  of term                      (* value abstraction *)
   | uapp of term & typ & typ          (* universal application *)
   | uabs of term.                     (* universal abstraction *)

Coercion tyvar : nat >-> typ.
Coercion var : nat >-> term.

Notation "ty :->: ty'" := (tyfun ty ty') (at level 70, no associativity).
Notation "t @{ t' \: ty }" := (app t t' ty) (at level 60, no associativity).
Notation "{ t \: ty }@ ty'" := (uapp t ty ty') (at level 60, no associativity).

Fixpoint eqtyp t1 t2 :=
  match t1, t2 with
    | tyvar n, tyvar m => n == m
    | t1l :->: t1r, t2l :->: t2r => eqtyp t1l t2l && eqtyp t1r t2r
    | tyabs tl, tyabs tr => eqtyp tl tr
    | _, _ => false
  end.

Lemma eqtypP : Equality.axiom eqtyp.
Proof.
  move => t1 t2; apply: (iffP idP) => [| <-].
  - by elim: t1 t2 => [n | t1l IHt1l t1r IHt1r | t1 IHt1]
      [// m /eqP -> | //= t2l t2r /andP [] /IHt1l -> /IHt1r -> |
       // t2 /IHt1 ->].
  - by elim: t1 => //= t ->.
Defined.

Canonical typ_eqMixin := EqMixin eqtypP.
Canonical typ_eqType := Eval hnf in EqType typ typ_eqMixin.

Fixpoint shift_typ d c t :=
  match t with
    | tyvar n => tyvar (if c <= n then n + d else n)
    | tl :->: tr => shift_typ d c tl :->: shift_typ d c tr
    | tyabs t => tyabs (shift_typ d c.+1 t)
  end.

Notation subst_typv ts m n :=
  (shift_typ n 0 (nth (tyvar (m - n - size ts)) ts (m - n))) (only parsing).

Fixpoint subst_typ n ts t :=
  match t with
    | tyvar m => if n <= m then subst_typv ts m n else m
    | tl :->: tr => subst_typ n ts tl :->: subst_typ n ts tr
    | tyabs t => tyabs (subst_typ n.+1 ts t)
  end.

Fixpoint typemap (f : nat -> typ -> typ) n t :=
  match t with
    | var m => var m
    | tl @{tr \: ty} => typemap f n tl @{typemap f n tr \: f n ty}
    | abs t => abs (typemap f n t)
    | {t \: ty1}@ ty2 => {typemap f n t \: f n.+1 ty1}@ f n ty2
    | uabs t => uabs (typemap f n.+1 t)
  end.

Fixpoint shift_term d c t :=
  match t with
    | var n => var (if c <= n then n + d else n)
    | tl @{tr \: ty} => shift_term d c tl @{shift_term d c tr \: ty}
    | abs t => abs (shift_term d c.+1 t)
    | {t \: ty1}@ ty2 => {shift_term d c t \: ty1}@ ty2
    | uabs t => uabs (shift_term d c t)
  end.

Notation subst_termv ts m n n' :=
  (typemap (shift_typ n') 0
    (shift_term n 0
      (nth (var (m - n - size ts)) ts (m - n)))) (only parsing).

Fixpoint subst_term n n' ts t :=
  match t with
    | var m => if n <= m then subst_termv ts m n n' else m
    | tl @{tr \: ty} => subst_term n n' ts tl @{subst_term n n' ts tr \: ty}
    | abs t => abs (subst_term n.+1 n' ts t)
    | {t \: ty1}@ ty2 => {subst_term n n' ts t \: ty1}@ ty2
    | uabs t => uabs (subst_term n n'.+1 ts t)
  end.

Fixpoint typing (ctx : context typ) (t : term) (ty : typ) : bool :=
  match t, ty with
    | var n, _ => ctxindex ctx n ty
    | tl @{tr \: ty'}, _ => typing ctx tl (ty' :->: ty) && typing ctx tr ty'
    | abs t, tyl :->: tyr => typing (Some tyl :: ctx) t tyr
    | {t \: ty1}@ ty2, _ =>
      (ty == subst_typ 0 [:: ty2] ty1) && typing ctx t (tyabs ty1)
    | uabs t, tyabs ty => typing (ctxmap (shift_typ 1 0) ctx) t ty
    | _, _ => false
  end.

Reserved Notation "t ->r1 t'" (at level 70, no associativity).

Inductive reduction1 : relation term :=
  | red1fst ty t1 t2      : abs t1 @{t2 \: ty} ->r1 subst_term 0 0 [:: t2] t1
  | red1snd t ty1 ty2     : {uabs t \: ty1}@ ty2 ->r1
                            typemap (subst_typ^~ [:: ty2]) 0 t
  | red1appl t1 t1' t2 ty : t1 ->r1 t1' -> t1 @{t2 \: ty} ->r1 t1' @{t2 \: ty}
  | red1appr t1 t2 t2' ty : t2 ->r1 t2' -> t1 @{t2 \: ty} ->r1 t1 @{t2' \: ty}
  | red1abs t t'          : t ->r1 t' -> abs t ->r1 abs t'
  | red1uapp t t' ty1 ty2 : t ->r1 t' -> {t \: ty1}@ ty2 ->r1 {t' \: ty1}@ ty2
  | red1uabs t t'         : t ->r1 t' -> uabs t ->r1 uabs t'
  where "t ->r1 t'" := (reduction1 t t').

Notation reduction := [* reduction1].
Infix "->r" := reduction (at level 70, no associativity).

Hint Constructors reduction1.

Notation SN := (Acc (fun x y => reduction1 y x)).

Definition neutral (t : term) : bool :=
  match t with abs _ => false | uabs _ => false | _ => true end.

Ltac congruence' := move => /=; try (move: addSn addnS; congruence).

Lemma shift_zero_ty n t : shift_typ 0 n t = t.
Proof. by elim: t n; congruence' => m n; rewrite addn0 if_same. Qed.

Lemma shift_add_ty d c d' c' t :
  c <= c' <= c + d ->
  shift_typ d' c' (shift_typ d c t) = shift_typ (d' + d) c t.
Proof. case/andP; do 2 elimleq; elim: t c; congruence' => *; elimif_omega. Qed.

Lemma shift_shift_distr_ty d c d' c' t :
  c' <= c ->
  shift_typ d' c' (shift_typ d c t) = shift_typ d (d' + c) (shift_typ d' c' t).
Proof. elimleq; elim: t c'; congruence' => *; elimif_omega. Qed.

Lemma shift_subst_distr_ty n d c ts t :
  c <= n ->
  shift_typ d c (subst_typ n ts t) = subst_typ (d + n) ts (shift_typ d c t).
Proof.
  elimleq; elim: t n c; congruence' => v n c;
    elimif_omega; rewrite shift_add_ty; elimif_omega.
Qed.

Lemma subst_shift_distr_ty n d c ts t :
  n <= c ->
  shift_typ d c (subst_typ n ts t) =
  subst_typ n (map (shift_typ d (c - n)) ts) (shift_typ d (size ts + c) t).
Proof.
  elimleq; elim: t n; congruence' => v n; rewrite size_map; elimif_omega.
  - rewrite !nth_default ?size_map /=; elimif_omega.
  - rewrite -shift_shift_distr_ty // nth_map' /=.
    f_equal; apply nth_equal; rewrite size_map; elimif_omega.
Qed.

Lemma subst_nil_ty n t : subst_typ n [::] t = t.
Proof. elim: t n; congruence' => v n; rewrite nth_nil /=; elimif_omega. Qed.

Lemma subst_shift_cancel_ty1 n d c ts t :
  c <= n ->
  subst_typ n ts (shift_typ d c t) =
  subst_typ n (drop (c + d - n) ts)
    (shift_typ (d - minn (c + d - n) (size ts)) c t).
Proof.
  elimleq; elim: t c; congruence' => v c; rewrite size_drop nth_drop.
  case (leqP' d n); elimif_omega; elimleq.
  case (leqP' d.+1 (size ts)) => H0; elimif_omega.
  rewrite !nth_default //; ssromega.
Qed.

Lemma subst_shift_cancel_ty2 n d c ts t :
  n <= c <= n + size ts ->
  subst_typ n ts (shift_typ d c t) =
  subst_typ n (take (c - n) ts ++ drop (c + d - n) ts)
    (shift_typ (c + d - (n + size ts)) c t).
Proof.
  case/andP; elimleq => H; elim: t n; congruence' => v n.
  rewrite size_cat size_take size_drop nth_cat nth_drop
           size_take (minn_idPl H); elimif_omega; f_equal.
  - case (leqP' (c + d) (size ts)) => H0.
    + rewrite addn0; f_equal; first f_equal; ssromega.
    + rewrite subn0 !nth_default; first f_equal; ssromega.
  - rewrite nth_take; first apply nth_equal; elimif_omega.
Qed.

Lemma subst_shift_cancel_ty3 n d c ts t :
  c <= n -> size ts + n <= d + c ->
  subst_typ n ts (shift_typ d c t) = shift_typ (d - size ts) c t.
Proof.
  move => H H0; rewrite subst_shift_cancel_ty1 ?drop_oversize ?subst_nil_ty;
    f_equal; ssromega.
Qed.

Lemma subst_app_ty n xs ys t :
  subst_typ n xs (subst_typ (size xs + n) ys t) = subst_typ n (xs ++ ys) t.
Proof.
  elim: t n; congruence' => v n; rewrite size_cat nth_cat; elimif_omega.
  rewrite subst_shift_cancel_ty3; elimif_omega.
Qed.

Lemma subst_subst_distr_ty n m xs ys t :
  m <= n ->
  subst_typ n xs (subst_typ m ys t) =
  subst_typ m (map (subst_typ (n - m) xs) ys) (subst_typ (size ys + n) xs t).
Proof.
  elimleq; elim: t m; congruence' => v m; elimif_omega.
  - rewrite (@subst_shift_cancel_ty3 m) ?size_map 1?nth_default //=;
      elimif_omega.
  - rewrite size_map -shift_subst_distr_ty //= nth_map' /=.
    f_equal; apply nth_equal; rewrite size_map; elimif_omega.
Qed.

Lemma subst_subst_compose_ty n m xs ys t :
  m <= size xs ->
  subst_typ n xs (subst_typ (n + m) ys t) =
  subst_typ n (insert (map (subst_typ 0 (drop m xs)) ys) xs 0 m) t.
Proof.
  move => H; elim: t n; congruence' => v n.
  rewrite size_insert nth_insert size_map; elimif_omega.
  - by rewrite (maxn_idPr H) nth_default /= 1?addnCA ?leq_addr //= addKn addnC.
  - rewrite (nth_map (tyvar (v - size ys))) // shift_subst_distr_ty //
            addn0 subst_shift_cancel_ty1 //=; elimif_omega.
Qed.

Lemma typemap_compose f g n m t :
  typemap f n (typemap g m t) =
  typemap (fun i ty => f (i + n) (g (i + m) ty)) 0 t.
Proof.
  elim: t n m => //=.
  - by move => tl IHtl tr IHtr ty n m; rewrite IHtl IHtr.
  - by move => t IH n m; rewrite IH.
  - by move => t IH ty1 ty2 n m; rewrite IH.
  - move => t IH n m; rewrite {}IH; f_equal.
    elim: t (0) => //=; move: addSnnS; congruence.
Qed.

Lemma typemap_eq' f g n m t :
  (forall o t, f (o + n) t = g (o + m) t) -> typemap f n t = typemap g m t.
Proof.
  move => H; elim: t n m H => //=.
  - by move => tl IHtl tr IHtr ty n m H; f_equal; auto; apply (H 0).
  - by move => t IH n m H; f_equal; auto; rewrite -(add0n n) -(add0n m).
  - by move => t IH ty1 ty2 n m H; f_equal; auto; [apply (H 1) | apply (H 0)].
  - by move => t IH n m H; f_equal; apply IH => o ty; rewrite -!addSnnS.
Qed.

Lemma typemap_eq f g n t :
  (forall n t, f n t = g n t) -> typemap f n t = typemap g n t.
Proof. move => H; apply typemap_eq' => {t} o; apply H. Qed.

Lemma shifttyp_zero c t : typemap (shift_typ 0) c t = t.
Proof. elim: t c => /=; move: shift_zero_ty; congruence. Qed.

Lemma shifttyp_add d c d' c' t :
  c <= c' <= c + d ->
  typemap (shift_typ d') c' (typemap (shift_typ d) c t) =
  typemap (shift_typ (d' + d)) c t.
Proof.
  rewrite typemap_compose => H; apply typemap_eq' => {t} n t.
  by rewrite addn0 shift_add_ty // -addnA !leq_add2l.
Qed.

Lemma shifttyp_shifttyp_distr d c d' c' t :
  c' <= c ->
  typemap (shift_typ d') c' (typemap (shift_typ d) c t) =
  typemap (shift_typ d) (d' + c) (typemap (shift_typ d') c' t).
Proof.
  rewrite !typemap_compose => H; apply typemap_eq => {t} n t.
  by rewrite shift_shift_distr_ty ?leq_add2l // addnCA.
Qed.

Lemma shifttyp_substtyp_distr n d c ts t :
  c <= n ->
  typemap (shift_typ d) c (typemap (subst_typ^~ ts) n t) =
  typemap (subst_typ^~ ts) (d + n) (typemap (shift_typ d) c t).
Proof.
  rewrite !typemap_compose => H; apply typemap_eq => {t} n' t.
  by rewrite shift_subst_distr_ty ?leq_add2l // addnCA.
Qed.

Lemma substtyp_shifttyp_distr n d c ts t :
  n <= c ->
  typemap (shift_typ d) c (typemap (subst_typ^~ ts) n t) =
  typemap (subst_typ^~ (map (shift_typ d (c - n)) ts)) n
    (typemap (shift_typ d) (size ts + c) t).
Proof.
  rewrite !typemap_compose => H; apply typemap_eq => {t} n' t.
  by rewrite subst_shift_distr_ty ?leq_add2l // subnDl addnCA addnA.
Qed.

Lemma substtyp_substtyp_distr n m xs ys t :
  m <= n ->
  typemap (subst_typ^~ xs) n (typemap (subst_typ^~ ys) m t) =
  typemap (subst_typ^~ (map (subst_typ (n - m) xs) ys)) m
    (typemap (subst_typ^~ xs) (size ys + n) t).
Proof.
  rewrite !typemap_compose => H; apply typemap_eq => {t} n' t.
  by rewrite subst_subst_distr_ty ?leq_add2l // subnDl addnCA addnA.
Qed.

Lemma shift_typemap_distr f d c n t :
  shift_term d c (typemap f n t) = typemap f n (shift_term d c t).
Proof. elim: t c n => /=; congruence. Qed.

Lemma subst_shifttyp_distr n m d c ts t :
  c + d <= m ->
  subst_term n m ts (typemap (shift_typ d) c t) =
  typemap (shift_typ d) c (subst_term n (m - d) ts t).
Proof.
  elimleq; elim: t n c; congruence' => v n c; elimif_omega.
  rewrite -!shift_typemap_distr shifttyp_add; elimif_omega.
Qed.

Lemma shifttyp_subst_distr d c n m ts t :
  m <= c ->
  typemap (shift_typ d) c (subst_term n m ts t) =
  subst_term n m (map (typemap (shift_typ d) (c - m)) ts)
    (typemap (shift_typ d) c t).
Proof.
  by elimleq; elim: t n m; congruence' => v n m; elimif_omega;
    rewrite size_map -!shift_typemap_distr -shifttyp_shifttyp_distr // nth_map'.
Qed.

Lemma subst_substtyp_distr n m m' tys ts t :
  m' <= m ->
  subst_term n m ts (typemap (subst_typ^~ tys) m' t) =
  typemap (subst_typ^~ tys) m' (subst_term n (size tys + m) ts t).
Proof.
  elimleq; elim: t n m'; congruence' => v n m'; elimif_omega.
  rewrite -!shift_typemap_distr typemap_compose.
  f_equal; apply typemap_eq => {v n ts} n t.
  rewrite subst_shift_cancel_ty3; f_equal; ssromega.
Qed.

Lemma substtyp_subst_distr n m m' tys ts t :
  m <= m' ->
  typemap (subst_typ^~ tys) m' (subst_term n m ts t) =
  subst_term n m (map (typemap (subst_typ^~ tys) (m' - m)) ts)
    (typemap (subst_typ^~ tys) m' t).
Proof.
  elimleq; elim: t n m; congruence' => v n m; elimif_omega.
  by rewrite size_map -!shift_typemap_distr
             -shifttyp_substtyp_distr // (nth_map' (typemap _ _)).
Qed.

Lemma shift_zero n t : shift_term 0 n t = t.
Proof. by elim: t n => /=; congruence' => m n; rewrite addn0 if_same. Qed.

Lemma shift_add d c d' c' t :
  c <= c' <= c + d ->
  shift_term d' c' (shift_term d c t) = shift_term (d' + d) c t.
Proof. case/andP; do 2 elimleq; elim: t c; congruence' => *; elimif_omega. Qed.

Lemma shift_shift_distr d c d' c' t :
  c' <= c ->
  shift_term d' c' (shift_term d c t) =
  shift_term d (d' + c) (shift_term d' c' t).
Proof. elimleq; elim: t c'; congruence' => v c'; elimif_omega. Qed.

Lemma subst_shift_distr n m d c ts t :
  n <= c ->
  shift_term d c (subst_term n m ts t) =
  subst_term n m (map (shift_term d (c - n)) ts) (shift_term d (size ts + c) t).
Proof.
  elimleq; elim: t n m; congruence' => v n m; rewrite size_map; elimif_omega.
  - rewrite !nth_default ?size_map /=; elimif_omega.
  - rewrite shift_typemap_distr -shift_shift_distr // nth_map' /=.
    do 2 f_equal; apply nth_equal; rewrite size_map; elimif_omega.
Qed.

Lemma shift_subst_distr n m d c ts t :
  c <= n ->
  shift_term d c (subst_term n m ts t) =
  subst_term (d + n) m ts (shift_term d c t).
Proof.
  elimleq; elim: t m c; congruence' => v m c; elimif_omega.
  rewrite shift_typemap_distr shift_add; elimif_omega.
Qed.

Lemma subst_shift_cancel n m d c ts t :
  c <= n -> size ts + n <= d + c ->
  subst_term n m ts (shift_term d c t) = shift_term (d - size ts) c t.
Proof.
  do 2 elimleq; elim: t m c; congruence' => v m c; elimif_omega.
  rewrite nth_default /=; f_equal; ssromega.
Qed.

Lemma subst_subst_distr n n' m m' xs ys t :
  n' <= n -> m' <= m ->
  subst_term n m xs (subst_term n' m' ys t) =
  subst_term n' m' (map (subst_term (n - n') (m - m') xs) ys)
    (subst_term (size ys + n) m xs t).
Proof.
  do 2 elimleq; elim: t n' m'; congruence' => v n' m'; elimif_omega.
  - rewrite nth_default /=; elimif_omega.
    rewrite -!shift_typemap_distr (@subst_shift_cancel n') // size_map;
      elimif_omega.
  - rewrite -!shift_typemap_distr -shift_subst_distr //
            subst_shifttyp_distr; elimif_omega.
    rewrite nth_map' /=; do 2 f_equal;
      apply nth_equal; rewrite !size_map; elimif_omega.
Qed.

Lemma subst_app n m xs ys t :
  subst_term n m xs (subst_term (size xs + n) m ys t) =
  subst_term n m (xs ++ ys) t.
Proof.
  elim: t n m; congruence' => v n m; rewrite nth_cat size_cat; elimif_omega.
  rewrite -!shift_typemap_distr subst_shift_cancel; elimif_omega.
Qed.

Lemma subst_nil n m t : subst_term n m [::] t = t.
Proof.
  elim: t n m; congruence' => v n m; rewrite nth_nil /= -fun_if; elimif_omega.
Qed.

Lemma subst_shifttyp_app n m m' ts t :
  subst_term n m (map (typemap (shift_typ m') 0) ts) t =
  subst_term n (m' + m) ts t.
Proof.
  elim: t n m; congruence' => v n m; rewrite size_map; elimif_omega.
  rewrite -!shift_typemap_distr !(nth_map' (typemap _ _)) /=; do 2 f_equal.
  elim: ts => //= t ts ->; f_equal.
  rewrite typemap_compose; apply typemap_eq => {n t ts} n t.
  rewrite addn0 shift_add_ty; elimif_omega.
Qed.

Lemma redappl t1 t1' t2 ty : t1 ->r t1' -> t1 @{t2 \: ty} ->r t1' @{t2 \: ty}.
Proof. apply (rtc_map' (fun x y => @red1appl x y t2 ty)). Qed.

Lemma redappr t1 t2 t2' ty : t2 ->r t2' -> t1 @{t2 \: ty} ->r t1 @{t2' \: ty}.
Proof. apply (rtc_map' (fun x y => @red1appr t1 x y ty)). Qed.

Lemma redapp t1 t1' t2 t2' ty :
  t1 ->r t1' -> t2 ->r t2' -> t1 @{t2 \: ty} ->r t1' @{t2' \: ty}.
Proof.
  by move => H H0; apply rtc_trans' with (t1' @{t2 \: ty});
    [apply redappl | apply redappr].
Qed.

Lemma redabs t t' : t ->r t' -> abs t ->r abs t'.
Proof. apply (rtc_map' red1abs). Qed.

Lemma reduapp t t' ty1 ty2 : t ->r t' -> {t \: ty1}@ ty2 ->r {t' \: ty1}@ ty2.
Proof. apply (rtc_map' (fun x y => @red1uapp x y ty1 ty2)). Qed.

Lemma reduabs t t' : t ->r t' -> uabs t ->r uabs t'.
Proof. apply (rtc_map' red1uabs). Qed.

Hint Resolve redappl redappr redapp redabs reduapp reduabs.

Lemma shifttyp_reduction1 t t' d c :
  t ->r1 t' -> typemap (shift_typ d) c t ->r1 typemap (shift_typ d) c t'.
Proof.
  move => H; move: t t' H d c.
  refine (reduction1_ind _ _ _ _ _ _ _) => /=; try by constructor.
  - by move => ty t1 t2 d c; rewrite shifttyp_subst_distr //= subn0.
  - by move => t ty1 ty2 d c; rewrite substtyp_shifttyp_distr //= subn0 add1n.
Qed.

Lemma shift_reduction1 t t' d c :
  t ->r1 t' -> shift_term d c t ->r1 shift_term d c t'.
Proof.
  move => H; move: t t' H d c.
  refine (reduction1_ind _ _ _ _ _ _ _) => /=; try by constructor.
  - by move => ty t1 t2 d c; rewrite subst_shift_distr //= subn0 add1n.
  - by move => t ty1 ty2 d c; rewrite shift_typemap_distr.
Qed.

Lemma substtyp_reduction1 t t' tys n :
  t ->r1 t' ->
  typemap (subst_typ^~ tys) n t ->r1 typemap (subst_typ^~ tys) n t'.
Proof.
  move => H; move: t t' H tys n.
  refine (reduction1_ind _ _ _ _ _ _ _) => /=; try by constructor.
  - by move => ty t1 t2 tys n;
      rewrite substtyp_subst_distr // subn0; constructor.
  - by move => t ty1 ty2 tys n; rewrite substtyp_substtyp_distr //= add1n subn0.
Qed.

Lemma subst_reduction1 t t' n m ts :
  t ->r1 t' -> subst_term n m ts t ->r1 subst_term n m ts t'.
Proof.
  move => H; move: t t' H n m ts.
  refine (reduction1_ind _ _ _ _ _ _ _) => /=; try by constructor.
  - by move => ty t1 t2 n m ts; rewrite subst_subst_distr //= !subn0.
  - by move => t ty1 ty2 n m ts; rewrite subst_substtyp_distr.
Qed.

Lemma subst_reduction t n m ts :
  Forall (fun t => t.1 ->r t.2) ts ->
  subst_term n m (unzip1 ts) t ->r subst_term n m (unzip2 ts) t.
Proof.
  move => H; elim: t n m => //=;
    auto => v n m; rewrite !size_map; elimif_omega.
  elim: ts v H => //=; case => t t' ts IH [[H _] | v] //=.
  - move: H.
    apply (rtc_map' (f := fun x =>
      typemap (shift_typ m) 0 (shift_term n 0 x))) => t1 t2 H.
    by apply shifttyp_reduction1, shift_reduction1.
  - by move => [_ H]; rewrite subSS; apply IH.
Qed.

Lemma ctxleq_preserves_typing ctx1 ctx2 t ty :
  ctx1 <=c ctx2 -> typing ctx1 t ty -> typing ctx2 t ty.
Proof.
  elim: t ty ctx1 ctx2 =>
    [n | tl IHtl tr IHtr tty | t IHt [] | t IHt ty1 ty2 | t IHt []] //=.
  - by move => ty ctx1 ctx2 /ctxleqP; apply.
  - by move => ty ctx1 ctx2 H /andP [] /(IHtl _ _ _ H) ->; apply IHtr.
  - by move => tyl tyr ctx1 ctx2 H; apply IHt; rewrite ctxleqE eqxx.
  - by move => ty ctx1 ctx2 H /andP [] ->; apply IHt.
  - by move => ty ctx1 ctx2 H; apply IHt, ctxleq_map.
Qed.

Section CRs.
Variable (P : term -> Prop).
Definition CR1 := forall t, P t -> SN t.
Definition CR2 := forall t t', t ->r1 t' -> P t -> P t'.
Definition CR3 := forall t,
  neutral t -> (forall t', t ->r1 t' -> P t') -> P t.
End CRs.

Record RC (P : term -> Prop) : Prop :=
  reducibility_candidate {
    rc_cr1 : CR1 P ;
    rc_cr2 : CR2 P ;
    rc_cr3 : CR3 P
  }.

Lemma CR2' P t t' : RC P -> t ->r t' -> P t -> P t'.
Proof.
  move => H; move: t t'.
  refine (clos_refl_trans_1n_ind _ _ _ _ _) => //= x y z H0 H1 H2 H3.
  by apply H2, (rc_cr2 H H0).
Qed.

Lemma CR4 P t : RC P ->
  neutral t -> (forall t', ~ t ->r1 t') -> P t.
Proof. by case => _ _ H H0 H1; apply H => // t' H2; move: (H1 _ H2). Qed.

Lemma CR4' P (v : nat) : RC P -> P v.
Proof. move => H; apply: (CR4 H) => // t' H0; inversion H0. Qed.

Lemma snorm_isrc : RC SN.
Proof.
  constructor; move => /=; try tauto.
  - by move => t t' H []; apply.
  - by move => t H H0; constructor => t' H1; apply H0.
Qed.

Lemma rcfun_isrc tyl P Q :
  RC P -> RC Q -> RC (fun u => forall v, P v -> Q (u @{v \: tyl})).
Proof.
  move => H H0; constructor; move => /=.
  - move => t /(_ 0 (CR4' _ H)) /(rc_cr1 H0).
    by rewrite -/((fun t => t @{0 \: tyl}) t);
      apply acc_preservation => x y H1; constructor.
  - by move => t t' H1 H2 v /H2; apply (rc_cr2 H0); constructor.
  - move => t1 H1 H2 t2 H3; move: t2 {H3} (rc_cr1 H H3) (H3).
    refine (Acc_rect _ _) => t2 _ H3 H4.
    apply (rc_cr3 H0) => //= t3 H5; move: H1; inversion H5;
      subst => //= _; auto; apply H3 => //; apply (rc_cr2 H H9 H4).
Qed.

Fixpoint reducible ty (preds : seq (typ * (term -> Prop))) t : Prop :=
  match ty with
    | tyvar v => nth SN (unzip2 preds) v t
    | tyfun tyl tyr => forall t',
      reducible tyl preds t' ->
      reducible tyr preds (t @{t' \: subst_typ 0 (unzip1 preds) tyl})
    | tyabs ty => forall ty' P, RC P ->
      reducible ty ((ty', P) :: preds)
        ({t \: subst_typ 1 (unzip1 preds) ty}@ ty')
  end.

Lemma reducibility_isrc ty preds :
  Forall (fun p => RC (snd p)) preds -> RC (reducible ty preds).
Proof.
  elim: ty preds => /= [n | tyl IHtyl tyr IHtyr | ty IHty] preds.
  - elim: preds n => [| P preds IH []] /=.
    + move => n _; rewrite nth_nil; apply snorm_isrc.
    + by case.
    + by move => n [H H0]; apply IH.
  - by move => H; apply
      (@rcfun_isrc (subst_typ 0 (unzip1 preds) tyl));
      [apply IHtyl | apply IHtyr].
  - move => H; constructor.
    + move => /= t /(_ 0 SN snorm_isrc)
        /(rc_cr1 (IHty ((_, _) :: _) (conj snorm_isrc H))).
      rewrite -/((fun t => {t \: subst_typ 1 (unzip1 preds) ty}@ 0) t).
      by apply acc_preservation => x y H0; constructor.
    + move => /= t t' H0 H1 ty' P H2; move/(H1 ty'): (H2).
      by apply (rc_cr2 (IHty ((_, _) :: _) (conj H2 H))); constructor.
    + move => /= t H0 H1 ty' P H2.
      apply (rc_cr3 (IHty ((_, _) :: _) (conj H2 H))) => //= t' H3.
      by move: H0; inversion H3; subst => //= _; apply H1.
Qed.

Lemma shift_reducibility c ty preds preds' t :
  c <= size preds ->
  (reducible (shift_typ (size preds') c ty)
     (insert preds' preds (tyvar 0, SN) c) t <->
   reducible ty preds t).
Proof.
  elim: ty c preds t => [v | tyl IHtyl tyr IHtyr | ty IHty] c preds t H.
  - rewrite /= /unzip2 map_insert nth_insert size_map; elimif_omega.
  - by split => /= H0 t' /(IHtyl c _ _ H) /H0 /(IHtyr c _ _ H); rewrite
      /unzip1 map_insert subst_shift_cancel_ty2 /= ?subn0 ?add0n ?size_insert
      ?size_map ?(leq_trans (leq_maxl _ _) (leq_addl _ _)) // take_insert
      size_map -[X in drop (c + X)](size_map (@fst _ _) preds') drop_insert
      subnDA addnK; (have ->: c - maxn c _ = 0 by ssromega);
      rewrite shift_zero_ty; move: H; rewrite -subn_eq0 => /eqP -> /=;
      rewrite cats0 cat_take_drop.
  - by split => /= H0 ty' P H1; apply (IHty c.+1 ((ty', P) :: preds));
      rewrite ?ltnS ?H //; move: {H0 H1} (H0 ty' P H1); rewrite /unzip1
        map_insert /= subst_shift_cancel_ty2 /= ?subn1 ?add1n ?ltnS ?size_insert
        ?size_map ?(leq_trans (leq_maxl _ _) (leq_addl _ _)) // addSn /=
        take_insert size_map -[X in drop (c + X)](size_map (@fst _ _) preds')
        drop_insert subSS subnDA addnK;
      (have ->: c - maxn c _ = 0 by ssromega); rewrite shift_zero_ty;
      move: H; rewrite -subn_eq0 => /eqP -> /=; rewrite cats0 cat_take_drop.
Qed.

Lemma subst_reducibility ty preds n tys t :
  n <= size preds ->
  (reducible (subst_typ n tys ty) preds t <->
   reducible ty
     (insert [seq (subst_typ 0 (unzip1 (drop n preds)) ty,
                   reducible ty (drop n preds)) | ty <- tys]
             preds (tyvar 0, SN) n)
     t).
Proof.
  elim: ty preds n tys t =>
    [v | tyl IHtyl tyr IHtyr | ty IHty] preds n tys t.
  - rewrite /= -(nth_map' (@snd _ _) (tyvar 0, SN)) /= nth_insert size_map.
    elimif_omega.
    + by rewrite nth_default ?leq_addr //= nth_map' addnC.
    + move => H0.
      rewrite (nth_map (tyvar (v - size tys))) //=.
      move: (shift_reducibility (nth (tyvar (v - size tys)) tys v)
        (take n preds) t (leq0n (size (drop n preds)))).
      rewrite /insert take0 drop0 sub0n /= cat_take_drop size_take.
      by move/minn_idPl: H0 => ->.
    + by rewrite nth_map' /=.
  - by move => H /=; split => H1 t' /IHtyl => /(_ H) /H1 /IHtyr => /(_ H);
      rewrite /unzip1 map_insert -map_comp /funcomp /=
              subst_subst_compose_ty ?map_drop // size_map.
  - move => /= H; split => H0 ty' P /(H0 ty' P) => {H0} H0.
    + rewrite /unzip1 map_insert -map_comp /funcomp /=.
      move/IHty: H0 => /= /(_ H).
      by rewrite /unzip1 subst_subst_compose_ty /insert /= ?subSS size_map
                 ?map_drop.
    + apply IHty => //; move: H0.
      by rewrite /unzip1 map_insert -map_comp /funcomp /= subst_subst_compose_ty
                 /insert /= ?subSS size_map ?map_drop.
Qed.

Lemma abs_reducibility t tyl tyr preds :
  Forall (fun p => RC (snd p)) preds ->
  (forall t',
   reducible tyl preds t' ->
   reducible tyr preds (subst_term 0 0 [:: t'] t)) ->
  reducible (tyl :->: tyr) preds (abs t).
Proof.
  move => /= H.
  move: (reducible tyl preds) (reducible tyr preds)
    (reducibility_isrc tyl H) (reducibility_isrc tyr H) => {H} P Q HP HQ.
  move => H t' H0.
  have H1: SN t by
    move: (rc_cr1 HQ (H _ H0));
      apply acc_preservation => x y; apply subst_reduction1.
  move: t H1 t' {H H0} (rc_cr1 HP H0) (H0) (H _ H0).
  refine (Acc_ind _ _) => t1 _ H; refine (Acc_ind _ _) => t2 _ H0 H1 H2.
  apply rc_cr3 => // t' H3; inversion H3; subst => //.
  - inversion H8; subst; apply H; auto.
    + apply (rc_cr1 HP H1).
    + by apply (rc_cr2 HQ (subst_reduction1 0 0 [:: t2] H5)).
  - apply H0 => //; first by apply (rc_cr2 HP H8).
    move: H2; apply (CR2' HQ).
    apply (@subst_reduction t1 0 0 [:: (t2, t2')]) => //=; split => //.
    by apply rtc_step.
Qed.

Lemma uabs_reducibility t ty preds :
  Forall (fun p => RC (snd p)) preds ->
  (forall v P, RC P ->
   reducible ty ((v, P) :: preds) (typemap (subst_typ^~ [:: v]) 0 t)) ->
  reducible (tyabs ty) preds (uabs t).
Proof.
  move => /= H H0 ty' P H1.
  move: {H0} (@reducibility_isrc ty ((ty', P) :: preds)) (H0 ty' P H1)
    => /= /(_ (conj H1 H)).
  move: {P H H1} (reducible _ _) => P H H0.
  have H1: SN t by
    move: (rc_cr1 H H0);
      apply acc_preservation => x y; apply substtyp_reduction1.
  move: t H1 H0; refine (Acc_ind _ _) => t _ H0 H1.
  apply (rc_cr3 H) => //= t' H2; inversion H2; subst => //.
  inversion H7; subst; apply H0 => //.
  apply (rc_cr2 H (substtyp_reduction1 _ _ H4) H1).
Qed.

Lemma uapp_reducibility t ty ty' preds :
  Forall (fun p => RC p.2) preds -> reducible (tyabs ty) preds t ->
  reducible (subst_typ 0 [:: ty'] ty) preds
    ({t \: subst_typ 1 (unzip1 preds) ty}@ subst_typ 0 (unzip1 preds) ty').
Proof.
  move => /= H H0.
  apply subst_reducibility => //=.
  rewrite /insert take0 sub0n drop0 /=.
  by apply H0, reducibility_isrc.
Qed.

Lemma reduce_lemma ctx preds t ty :
  typing [seq Some c.2 | c <- ctx] t ty ->
  Forall (fun p => RC p.2) preds ->
  Forall (fun c => reducible c.2 preds c.1) ctx ->
  reducible ty preds
    (subst_term 0 0 (unzip1 ctx) (typemap (subst_typ^~ (unzip1 preds)) 0 t)).
Proof.
  elim: t ty ctx preds => /=.
  - move => v ty ctx preds H H0 H1.
    rewrite shifttyp_zero shift_zero subn0 size_map.
    elim: ctx v H H1 => //=; first by case.
    case => t ty' ctx IH [] //=.
    + by case/eqP => <- [].
    + by move => v H [H1 H2]; rewrite subSS; apply IH.
  - move => tl IHtl tr IHtr tty ty ctx preds /andP [H H0] H1 H2.
    by move: (IHtl (tty :->: ty) ctx preds H H1 H2) => /=; apply; apply IHtr.
  - move => t IHt [] // tyl tyr ctx preds H H0 H1.
    apply abs_reducibility => // t' H2.
    rewrite subst_app //=; apply (IHt tyr ((t', tyl) :: ctx)) => //.
  - move => t IHt ttyl ttyr ty ctx preds /andP [] /eqP -> {ty} H H0 H1.
    by apply uapp_reducibility => //; apply IHt.
  - move => t IHt [] // ty ctx preds H H0 H1.
    apply uabs_reducibility => // v P H2.
    rewrite -(subst_substtyp_distr 0 [:: v]) // typemap_compose /=.
    have /(typemap_eq 0 t) -> : forall i ty,
      subst_typ (i + 0) [:: v] (subst_typ (i + 1) (unzip1 preds) ty) =
      subst_typ i (unzip1 ((v, P) :: preds)) ty by
        move => i ty'; rewrite addn0 addn1 subst_app_ty.
    move: (IHt ty
      (map (fun c => (c.1, shift_typ 1 0 c.2)) ctx) ((v, P) :: preds)).
    rewrite /unzip1 -!map_comp /funcomp /=; apply => //=.
    + by move: H; rewrite -map_comp /funcomp /=.
    + elim: ctx H1 {t ty IHt H H0 H2} => //=;
        case => t ty ctx IH [] H H0; split => /=; last by apply IH.
      case: (shift_reducibility ty [:: (v, P)] t (leq0n (size preds))) => _.
      by rewrite /insert take0 drop0 sub0n /=; apply.
Qed.

Theorem typed_term_is_snorm ctx t ty : typing ctx t ty -> SN t.
Proof.
  move => H.
  move: (@reduce_lemma
    (map (oapp (pair (var 0)) (var 0, tyvar 0)) ctx) [::] t ty) => /=.
  rewrite -map_comp /funcomp /=.
  have {H} H: typing
    [seq Some (oapp (pair (var 0)) (var 0, tyvar 0) x).2 | x <- ctx] t ty by
    move: H; apply ctxleq_preserves_typing;
      elim: ctx {t ty} => //; case => // ty ctx H; rewrite ctxleqE eqxx /=.
  move/(_ H I) {H}.
  have H: Forall (fun c => reducible c.2 [::] c.1)
                 (map (oapp (pair (var 0)) (var 0, tyvar 0)) ctx) by
    elim: ctx {t ty} => //= ty ctx IH; split => // {IH};
      rewrite /oapp /snd; case: ty => [ty |]; apply CR4', reducibility_isrc.
  move/(_ H) => {H} /(rc_cr1 (reducibility_isrc _ _)) /= /(_ I).
  set f := subst_term _ _ _; set g := typemap _ _.
  rewrite -/((fun t => f (g t)) t); apply acc_preservation => x y H.
  by rewrite {}/f {}/g; apply subst_reduction1, substtyp_reduction1.
Qed.