From Coq Require Import Lia List Init.Nat.
From PCF2.Autosubst Require Import pcf_2 unscoped.
From PCF2 Require Import pcf_2_system pcf_2_contexts pcf_2_utils CE CE_facts SATIS SATIS_facts preliminaries.
From PCF2.external Require Import SR.
From PCF2.external.Synthetic Require Import Definitions.
Set Default Goal Selector "!".

Definition ren_shift (d1 d2 e f: str) :=
  fun n =>
  if ltb n (2 * length d1) then 2 * length e + 2 + n else
    if ltb n (2 * (length d1 + length e)) then n - 2 * length d1 else
      if ltb n (2 * (length d1 + length e + length d2)) then
        2 * (length e) + 2 + (n - 2 * diff (length e) (length f)) else
          if ltb n (2 * (length d1 + length e + length d2) + 2) then
            n - 2 * (length d1 + length d2) else
            n + 2 * length f + 2.

Lemma ren_shift_well_typed (d1 d2 e f: str) R W0:
  ren_well_typed (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2) ++ make_rule_types R ++ T W0 :: nil) (base_context (2 * length (d1 ++ e ++ d2) + 2) ++ make_rule_types R ++ T W0 :: nil) (ren_shift d1 d2 e f).
Proof.
  intros n A H. assert (eq1: n < 2 * length (d1 ++ e ++ d2) + 2 + length R + 1).
  { assert (eq1: 2 * length (d1 ++ e ++ d2) + 2 + length R + 1 = length (base_context (2 * length (d1 ++ e ++ d2) + 2) ++ make_rule_types R ++ T W0 :: nil)).
    - repeat rewrite app_length. rewrite length_base_context. rewrite make_rule_types_length. cbn. lia.
    - rewrite eq1. apply nth_error_Some. intros H1. now rewrite H1 in H. }
  unfold ren_shift. destruct (ltb n (2 * length d1)) eqn: eq2.
  { rewrite ltb_lt_true in eq2. rewrite nth_error_app2. 2: rewrite length_base_context; lia.
    rewrite nth_error_app1 in H. 2: rewrite length_base_context; simpl_list; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto. rewrite nth_error_app1. 2: rewrite length_base_context; simpl_list; lia. apply base_context_le_base. simpl_list. lia. }
    rewrite ltb_lt_false in eq2. destruct (ltb n (2 * (length d1 + length e))) eqn: eq3.
  { rewrite ltb_lt_true in eq3. rewrite nth_error_app1. 2: rewrite length_base_context; lia.
  rewrite nth_error_app1 in H. 2: rewrite length_base_context; simpl_list; lia.
  erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list. lia. }
  rewrite ltb_lt_false in eq3. destruct (ltb n (2 * (length d1 + length e + length d2))) eqn: eq4.
  { rewrite ltb_lt_true in eq4. destruct (nat_ord_dec (length f) (length e)) as [l | l].
    - specialize (diff1 _ _ l). intros H1. rewrite nth_error_app2. 2: rewrite H1; rewrite length_base_context; lia.
    rewrite nth_error_app1 in H. 2: rewrite length_base_context; simpl_list; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto.
    rewrite nth_error_app1. 2: rewrite length_base_context, H1; simpl_list.
    2: { destruct (arith_technical' (2 * (length d1 + length e)) n (2 * length d2)) as [n' [H2 H3]]. 1,2 : lia.
         rewrite H3. lia. } apply base_context_le_base. simpl_list.
    rewrite H1. lia.
    - specialize (diff2 _ _ l). intros H1. rewrite nth_error_app2. 2: rewrite H1; rewrite length_base_context; lia.
    rewrite nth_error_app1 in H. 2: rewrite length_base_context; simpl_list; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto.
    rewrite nth_error_app1. 2: rewrite H1, length_base_context; simpl_list; lia. apply base_context_le_base. simpl_list.
    rewrite H1. lia. }
    rewrite ltb_lt_false in eq4. destruct (ltb n (2 * (length d1 + length e + length d2) + 2)) eqn: eq5.
    - rewrite ltb_lt_true in eq5. rewrite nth_error_app1. 2: rewrite length_base_context; lia.
      rewrite nth_error_app1 in H. 2: rewrite length_base_context; simpl_list; lia.
    erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list. lia.
    - rewrite ltb_lt_false in eq5. repeat rewrite app_length in eq1. rewrite nth_error_app2. 2: rewrite length_base_context; lia.
      rewrite nth_error_app2. 2: repeat rewrite length_base_context; simpl_list; lia.
      rewrite nth_error_app2 in H. 2: rewrite length_base_context; simpl_list; lia.
      rewrite length_base_context in H. repeat rewrite length_base_context.
      assert (eq6: n + 2 * length f + 2 - (2 * length e + 2) - (2 * length (d1 ++ f ++ d2) + 2) = n - (2 * length (d1 ++ e ++ d2) + 2)) by now simpl_list; lia.
      now rewrite eq6.
Qed.

Lemma ren_shift_well_typed' (d1 d2 e f: str):
  ren_well_typed (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) (base_context (2 * length (d1 ++ e ++ d2) + 2)) (ren_shift d1 d2 e f).
Proof.
  intros n A H. assert (eq1: n < 2 * length (d1 ++ e ++ d2) + 2).
  { rewrite <- length_base_context. apply nth_error_Some. intros H1. now rewrite H1 in H. }
  unfold ren_shift. destruct (ltb n (2 * length d1)) eqn: eq2.
  { rewrite ltb_lt_true in eq2. rewrite nth_error_app2. 2: rewrite length_base_context; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list. lia. }
  rewrite ltb_lt_false in eq2. destruct (ltb n (2 * (length d1 + length e))) eqn: eq3.
  { rewrite ltb_lt_true in eq3. rewrite nth_error_app1. 2: rewrite length_base_context; lia.
  erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list. lia. }
  rewrite ltb_lt_false in eq3. destruct (ltb n (2 * (length d1 + length e + length d2))) eqn: eq4.
  { rewrite ltb_lt_true in eq4. destruct (nat_ord_dec (length f) (length e)) as [l | l].
    - specialize (diff1 _ _ l). intros H1. rewrite nth_error_app2. 2: rewrite H1; rewrite length_base_context; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list.
    rewrite H1. lia.
    - specialize (diff2 _ _ l). intros H1. rewrite nth_error_app2. 2: rewrite H1; rewrite length_base_context; lia.
    rewrite length_base_context. erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list.
    rewrite H1. lia. }
    rewrite ltb_lt_false in eq4. destruct (ltb n (2 * (length d1 + length e + length d2) + 2)) eqn: eq5.
    - rewrite ltb_lt_true in eq5. rewrite nth_error_app1. 2: rewrite length_base_context; lia.
    erewrite (base_context_some_base _ _ A). 2: eauto. apply base_context_le_base. simpl_list. lia.
    - rewrite ltb_lt_false in eq5. repeat rewrite app_length in eq1. lia.
Qed.

Lemma t_subst_map_var_id'' (enc: str -> tm) (R: list (str * str)) (F: str * str -> tm) (W0 d1 f d2: str):
  map (Subst_tm (t_subst enc R F W0 (d1 ++ f ++ d2))) (var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * length (d1 ++ f ++ d2)) 2) = var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * length (d1 ++ f ++ d2)) 2.
Proof.
  apply list_eq.
  1: now rewrite map_length.
  intros n a a' H1 H2.
  rewrite nth_error_map in H1.
  assert (H3: n < 2 * length f + 2).
  { assert (length (var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * length (d1 ++ f ++ d2)) 2) = 2 * length f + 2) by now rewrite app_length, length_var_seq, length_var_seq; lia.
    rewrite <- H. apply nth_error_Some. intros H3. now rewrite H3 in H2. }
  destruct (ltb n (2 * length f)) eqn: e1.
  { rewrite ltb_lt_true in e1. rewrite nth_error_app1 in H2. 2: rewrite length_var_seq; lia.
    rewrite var_seq_nth in H2. 2: easy. injection H2. intros ?; subst. rewrite nth_error_app1 in H1. 2: now rewrite length_var_seq.
    rewrite var_seq_nth in H1. 2: easy. cbn in H1. injection H1. intros ?. subst. unfold t_subst.
    destruct (leb (length d1 + (length d1 + 0) + n)(2 * length (d1 ++ f ++ d2) + 1)) eqn: e2. 1: easy.
    rewrite leb_le_false in e2. repeat rewrite app_length in e2. lia. }
    rewrite ltb_lt_false in e1. rewrite nth_error_app2 in H2. 2: rewrite length_var_seq; lia.
    rewrite nth_error_app2 in H1. 2: rewrite length_var_seq; lia.
    rewrite var_seq_nth in H2. 2: rewrite length_var_seq; lia.
    rewrite var_seq_nth in H1. 2: rewrite length_var_seq; lia.
    injection H2. injection H1. intros ? ?. subst. repeat rewrite length_var_seq.
    unfold t_subst. destruct (leb (length (d1 ++ f ++ d2) + (length (d1 ++ f ++ d2) + 0) + (n - (length f + (length f + 0))))(2 * length (d1 ++ f ++ d2) + 1)) eqn: e2.
    1: easy. rewrite leb_le_false in e2. lia.
Qed.

Lemma t_subst_rule (enc: str -> tm) (R: list (str * str)) (F: str * str -> tm) (W0 W: str) (p: str * str) (n: nat):
  nth_error R n = Some p -> (t_subst enc R F W0 W) (2 * length W + 2 + n) = F p.
Proof.
  intros H. unfold t_subst. destruct (leb (2 * length W + 2 + n) (2 * length W + 1)) eqn: e1.
  { rewrite leb_le_true in e1. lia. }
  rewrite leb_le_false in e1. destruct (leb (2 * length W + 2 + n) (2 * length W + 1 + length R)) eqn: e2.
  - assert (eq: 2 * length W + 2 + n - (2 * length W + 2) = n) by lia. destruct (nth_error R (2 * length W + 2 + n - (2 * length W + 2))) eqn: e3.
    + rewrite eq in e3. rewrite e3 in H.
      injection H. intros?. now subst.
    + rewrite eq in e3. rewrite e3 in H. discriminate.
  - rewrite leb_le_false in e2. enough (n < length R) by lia.
    apply nth_error_Some. intros H'. rewrite H' in H. discriminate.
Qed.

Lemma ren_shift_typed (t: tm) (d1 d2 e f: str) (R: SRS bool) (W0: str):
  (base_context (2 * length (d1 ++ e ++ d2) + 2) ++ make_rule_types R ++ T W0 :: nil) ⊢ t: Base
  -> (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2) ++ make_rule_types R ++ T W0 :: nil) ⊢ ren_tm (ren_shift d1 d2 e f) t: Base.
Proof.
  intros H. eapply ren_preserves'. 2: exact H. eapply ren_shift_well_typed.
Qed.

Lemma ren_shift_shifted_t_subst_char enc R F (d1 e f d2 W0: str) t:
  Subst_tm (iter (2 * length e + 2) Up_tm_tm (t_subst enc R F W0 (d1 ++ f ++ d2))) (ren_tm (ren_shift d1 d2 e f) t) = ren_tm (ren_shift d1 d2 e f) (Subst_tm (t_subst enc R F W0 (d1 ++ e ++ d2)) t).
Proof.
  asimpl. apply subst_charact.
  intros n. unfold ren_shift, t_subst, core.funcomp.
Admitted.

Lemma ren_var d1 e f d2:
  map (ren_tm (ren_shift d1 d2 e f)) (var_seq 0 (2 * length (d1 ++ e ++ d2) + 2)) = var_seq (2 * length e + 2) (2 * length d1) ++ var_seq 0 (2 * length e) ++ var_seq (2 * (length e + length d1 + length f) + 2) (2 * length d2) ++ var_seq (2 * length e) 2.
Proof.
Admitted.

Lemma derived_satis_ineq (d1 e f d2: str) enc R W0 F t v:
  word_encoding enc v -> (base_context (2 * length (d1 ++ e ++ d2) + 2)) ⊢ apply_args (enc (d1 ++ e ++ d2)) (var_seq 0 (2 * length (d1 ++ e ++ d2) + 2)) ≤ Subst_tm (t_subst enc R F W0 (d1 ++ e ++ d2)) t : Base
  -> (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) ⊢ apply_args (enc (d1 ++ e ++ d2)) (var_seq (2 * length e + 2) (2 * length d1) ++ var_seq 0 (2 * length e) ++ var_seq (2 * (length e + length d1 + length f) + 2) (2 * length d2) ++ var_seq (2 * length e) 2) ≤ Subst_tm (iter (2 * length e + 2) Up_tm_tm (t_subst enc R F W0 (d1 ++ f ++ d2))) (ren_tm (ren_shift d1 d2 e f) t) : Base.
Proof.
  intros enc_val H. rewrite ren_shift_shifted_t_subst_char. rewrite <- ren_var.
  erewrite <- (closed_ren (enc (d1 ++ e ++ d2))) with (f := ren_shift d1 d2 e f).
  2: { eapply typed_empty_closed. eapply enc_typed. eauto. }
  rewrite <- ren_apply_args. eapply ineq_ren. 1: apply ren_shift_well_typed'.
  easy.
Qed.

Lemma context_existence (s: tm) (d1 e f d2: str):
  nil ⊢ s: T e ⟶ T f -> exists C, ctxt_typed C (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) Base (base_context (2 * length (d1 ++ f ++ d2) + 2)) Base /\ forall t, fill C t = apply_args (app s (lam_T (2 * length e + 2) t)) (var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * length (d1 ++ f ++ d2)) 2).
Proof.
Admitted.

Lemma shift_t_subst_well_typed (enc: str -> tm) (R: list (str * str)) (F: str * str -> tm) (W0 d1 e f d2: str):
  subst_well_typed (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) (base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2) ++ ((make_rule_types R)) ++ (cons (T W0) nil)) (iter (2 * length e + 2) Up_tm_tm (t_subst enc R F W0 (d1 ++ f ++ d2))).
Proof.
Admitted.

Lemma reduces_SR_SATIS_forward (E: list (val_word_enc)) (R: list (str * str)):
  forall p, SR R p -> SATIS E R p.
Proof.
  intros [W0 W] H.
  induction H as [W0 | W0 W W'].
  - unfold SATIS. exists (apply_args (var_tm (2 * length W0 + length R + 2)) (var_seq 0 (2 * length W0 + 2))).
    split.
    + eapply apply_args_typed with (l1 := base_context (2 * length W0 +2)).
      * rewrite <- T_list_to_fun. constructor. rewrite nth_error_app2.
        2: rewrite length_base_context; lia. rewrite nth_error_app2.
        2: rewrite length_base_context, make_rule_types_length; lia.
        rewrite length_base_context, make_rule_types_length.
        assert (eq1: 2 * length W0 + length R + 2 - (2 * length W0 + 2) - length R = 0) by lia.
        now rewrite eq1.
      * now rewrite length_base_context, length_var_seq.
      * intros n A t H1 H2. assert (n < 2 * length W0 + 2).
        { rewrite <- length_base_context. apply nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length W0 + 2)) n). }
        rewrite var_seq_nth in H2. 2: easy.
        injection H2. intros ?. subst. constructor. rewrite nth_error_app1. 2: now rewrite length_base_context.
        easy.
    + rewrite Forall_forall. intros [[enc v] enc_val] H f f_enc. cbn in *.
      assert (eq1: apply_args (var_tm (2 * length W0 + length R + 2)) (var_seq 0 (2 * length W0 + 2)) = fold_right (fun arg t : tm => app t arg) (var_tm (length W0 + (length W0 + 0) + length R + 2)) (rev (map (fun n : nat => var_tm n) (seq 0 (length W0 + (length W0 + 0) + 2))))) by easy.
      rewrite <- eq1. unfold satisfies. rewrite subst_apply_args.
      rewrite t_subst_map_var_id. asimpl. rewrite t_subst_initial.
      eapply obs_preorder_refl. eapply apply_args_typed with (l1 := base_context (2 * length W0 +2)).
      * rewrite <- T_list_to_fun. assert (eq2: base_context (2 * length W0 + 2) = nil ++ base_context (2 * length W0 + 2)) by easy.
        rewrite eq2. apply type_weakening. eapply enc_typed; eauto.
      * now rewrite length_base_context, length_var_seq.
      * intros n A t H1 H2. assert (n < 2 * length W0 + 2).
        { rewrite <- length_base_context. apply nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length W0 + 2)) n). }
        rewrite var_seq_nth in H2. 2: easy.
        injection H2. intros ?. subst. now constructor.
  - destruct IHrewt as [t [typed_t Ht]].
    inversion H0 as [d1 d2 e f]. destruct (In_nth_error _ _ H1) as [n Hn].
    exists (apply_args (app (var_tm (2 * length W' + 2 + n)) (lam_T (2 * length e + 2) (ren_tm (ren_shift d1 d2 e f) t))) (var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * length W') 2)).
    split.
    + apply apply_args_typed with (l1 := base_context (2 * length f + 2)).
      * apply app_typed with (typ1 := T e).
        -- rewrite <- T_list_to_fun. constructor. rewrite nth_error_app2. 2: rewrite length_base_context, H3; lia.
           rewrite length_base_context, H3. assert (eq1: 2 * length W' + 2 + n - (2 * length W' + 2) = n) by lia.
           rewrite eq1. unfold make_rule_types. rewrite nth_error_app1.
           2: { rewrite map_length. apply nth_error_Some; intros H'. destruct (nth_error R n) eqn: eq2; discriminate. }
           rewrite nth_error_map. now rewrite Hn.
        -- rewrite (T_list_to_fun e). rewrite <- (base_context_rev (2 * length e + 2)).
           rewrite <- (length_base_context (2 * length e + 2)) at 1. eapply lam_list_to_type'.
           apply ren_shift_typed. now rewrite H2.
      * now rewrite length_base_context, app_length, length_var_seq, length_var_seq.
      * intros n' A' t' H1' H2'. erewrite base_context_some_base; eauto.
        assert (e1: n' < 2 * length f + 2).
        { rewrite <- length_base_context. erewrite <- nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length f + 2)) n'). }
        destruct (nat_ord_dec (2 * length f) n').
        -- rewrite nth_error_app2 in H2'. 2: now rewrite length_var_seq.
           rewrite length_var_seq in H2'. assert (eq3: n' - 2 * length f < 2) by lia.
           rewrite var_seq_nth in H2'. 2: easy.
           injection H2'. intros eq. fold (2 * length W') in eq. fold (2 * length f) in eq.
           subst. constructor. rewrite nth_error_app1.
           2: rewrite length_base_context; lia. apply base_context_le_base. lia.
        -- rewrite nth_error_app1 in H2'. 2: now rewrite length_var_seq.
           rewrite var_seq_nth in H2'. 2: easy. injection H2'. intros eq.
           fold (2 * length d1) in eq. subst. constructor.
           rewrite nth_error_app1. 2: rewrite length_base_context; simpl_list; lia.
           rewrite base_context_le_base. 1: easy. simpl_list. lia.
    + rewrite Forall_forall. intros enc H' F HF.
      rewrite Forall_forall in Ht. specialize (Ht enc H' F HF).
      destruct enc as [[enc v] enc_val].
      assert (eq1: snd (proj1_sig (exist (fun p : (str -> tm) * bool => word_encoding (fst p) (snd p)) (enc, v) enc_val)) = v) by easy.
      assert (eq2: fst (proj1_sig (exist (fun p : (str -> tm) * bool => word_encoding (fst p) (snd p)) (enc, v) enc_val)) = enc) by easy.
      rewrite eq1, eq2 in *.
      unfold satisfies in *. rewrite subst_apply_args. asimpl.
      rewrite <- H3. rewrite t_subst_map_var_id''. erewrite t_subst_rule; eauto.
      unfold fun_rule_encoding in HF. rewrite Forall_forall in HF.
      destruct (context_existence (F(e, f)) d1 e f d2) as [C [HC1 HC2]].
      1: now apply HF.
      rewrite lam_T_shift_subst. rewrite <- HC2.
      eapply obs_preorder_trans.
      5: {eapply obs_preorder_context. 3: exact HC1.
      3: { eapply derived_satis_ineq. 1: eauto. now rewrite H2. }
      - eapply apply_args_typed with (l1 := base_context (2 * length (d1 ++ e ++ d2) + 2)).
        + rewrite <- T_list_to_fun. assert (eq3: base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2) = nil ++ base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) by easy.
          rewrite eq3. apply type_weakening. eapply enc_typed. eauto.
        + rewrite length_base_context. repeat rewrite app_length. repeat rewrite length_var_seq. lia.
        + intros n' A' t' H1' H2'. assert (eq3: n' < 2 * length (d1 ++ e ++ d2) + 2).
        { rewrite <- length_base_context. apply nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length (d1 ++ e ++ d2) + 2)) n'). }
        erewrite base_context_some_base. 2: eauto.
        destruct (nat_ord_dec (2 * length d1) n').
        2: { rewrite nth_error_app1 in H2'. 2: rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: easy.
             injection H2'. intros ?. subst. constructor. rewrite nth_error_app2. 2: rewrite length_base_context; lia. apply base_context_le_base. rewrite length_base_context. simpl_list. lia. }
        destruct (nat_ord_dec (2 * (length d1 + length e)) n').
        2: { rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app1 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: rewrite length_var_seq; lia.
             injection H2'. intros ?; subst. constructor. rewrite nth_error_app1. 2: rewrite length_var_seq, length_base_context; lia. apply base_context_le_base. rewrite length_var_seq; lia. }
        destruct (nat_ord_dec (2 * (length d1 + length e + length d2)) n').
        2: { rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite nth_error_app1 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: repeat rewrite length_var_seq; lia.
        repeat rewrite length_var_seq in H2'. destruct (arith_technical' (2 * (length d1 + length e)) n' (2 * length d2)) as [m [eqm Hm]].
        1, 2: lia. rewrite Hm in H2'. assert (eq4: 2 * (length e + length d1 + length f) + 2 + (2 * (length d1 + length e) + m - 2 * length d1 - 2 * length e) = 2 * (length e + length d1 + length f) + 2 + m) by lia.
        rewrite eq4 in H2'.
        injection H2'. intros ?; subst. constructor. rewrite nth_error_app2. 2: rewrite length_base_context; lia. apply base_context_le_base. rewrite length_base_context. simpl_list. lia. }
        rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia.
        repeat rewrite app_length in eq3. rewrite var_seq_nth in H2'.
        2: repeat rewrite length_var_seq; lia.
        injection H2'. intros ?; subst. constructor. repeat rewrite length_var_seq. rewrite nth_error_app1. 2: rewrite length_base_context; lia. apply base_context_le_base. lia.
        - eapply subst_preserves. 1: apply shift_t_subst_well_typed.
          eapply ren_preserves'. 1: apply ren_shift_well_typed. now rewrite H2.
   }
      * eapply apply_args_typed with (l1 := (base_context (2 * length (d1 ++ f ++ d2) + 2))).
        -- rewrite <- T_list_to_fun. assert (eq: base_context (2 * length (d1 ++ f ++ d2) + 2) = nil ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) by now simpl_list.
           rewrite eq. eapply type_weakening. eapply enc_typed. eauto.
        -- now rewrite length_base_context, length_var_seq.
        -- intros n' A' t' H1' H2'. erewrite base_context_some_base. 2: eauto.
           assert (H3': n' < 2 * length (d1 ++ f ++ d2) + 2).
           { rewrite <- length_base_context. apply nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length (d1 ++ f ++ d2) + 2)) n'). }
           erewrite var_seq_nth in H2'. 2: easy.
           injection H2'. intros ?; subst. constructor. now apply base_context_le_base.
      * eapply fill_type. 2: exact HC1. eapply apply_args_typed with (l1 := base_context (2 * length (d1 ++ e ++ d2) + 2)).
        -- assert (eq3: base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2) = nil ++ base_context (2 * length e + 2) ++ base_context (2 * length (d1 ++ f ++ d2) + 2)) by easy.
           rewrite eq3. apply type_weakening. rewrite <- T_list_to_fun. eapply enc_typed. eauto.
        -- simpl_list. repeat rewrite length_var_seq; rewrite length_base_context. lia.
        -- intros n' A' t' H1' H2'. assert (eq3: n' < 2 * length (d1 ++ e ++ d2) + 2).
           { rewrite <- length_base_context. apply nth_error_Some. intros ?. now destruct (nth_error (base_context (2 * length (d1 ++ e ++ d2) + 2)) n'). }
           erewrite base_context_some_base. 2: eauto.
           destruct (nat_ord_dec (2 * length d1) n').
           2: { rewrite nth_error_app1 in H2'. 2: rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: easy.
                injection H2'. intros ?. subst. constructor. rewrite nth_error_app2. 2: rewrite length_base_context; lia. apply base_context_le_base. rewrite length_base_context. simpl_list. lia. }
           destruct (nat_ord_dec (2 * (length d1 + length e)) n').
           2: { rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app1 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: rewrite length_var_seq; lia.
                injection H2'. intros ?; subst. constructor. rewrite nth_error_app1. 2: rewrite length_var_seq, length_base_context; lia. apply base_context_le_base. rewrite length_var_seq; lia. }
           destruct (nat_ord_dec (2 * (length d1 + length e + length d2)) n').
           2: { rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite nth_error_app1 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite var_seq_nth in H2'. 2: repeat rewrite length_var_seq; lia.
           repeat rewrite length_var_seq in H2'. destruct (arith_technical' (2 * (length d1 + length e)) n' (2 * length d2)) as [m [eqm Hm]].
           1, 2: lia. rewrite Hm in H2'. assert (eq4: 2 * (length e + length d1 + length f) + 2 + (2 * (length d1 + length e) + m - 2 * length d1 - 2 * length e) = 2 * (length e + length d1 + length f) + 2 + m) by lia.
           rewrite eq4 in H2'.
           injection H2'. intros ?; subst. constructor. rewrite nth_error_app2. 2: rewrite length_base_context; lia. apply base_context_le_base. rewrite length_base_context. simpl_list. lia. }
           rewrite nth_error_app2 in H2'. 2: rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia. rewrite nth_error_app2 in H2'. 2: repeat rewrite length_var_seq; lia.
           repeat rewrite app_length in eq3. rewrite var_seq_nth in H2'.
           2: repeat rewrite length_var_seq; lia.
           injection H2'. intros ?; subst. constructor. repeat rewrite length_var_seq. rewrite nth_error_app1. 2: rewrite length_base_context; lia. apply base_context_le_base. lia.
      * eapply fill_type. 2: exact HC1. eapply subst_preserves. 2: { eapply ren_preserves'. 2: eauto. rewrite <- H2. apply ren_shift_well_typed. }
        apply shift_t_subst_well_typed.
      * rewrite HC2. destruct (HF (e, f) H1) as [type_F [HF' _]].
        specialize (HF' d1 d2). cbn in HF'. unfold rule_ineq in HF'. exact HF'.
Qed.