Library MetaCoq.PCUIC.Syntax.PCUICDepth

From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool.
From MetaCoq.Template Require Import utils LibHypsNaming.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize PCUICInduction.
From Coq Require Import List.
From Equations Require Import Equations.
From Equations.Prop Require Import Subterm.
Import PCUICEnvTyping.

Definition def_depth_gen (depth : term nat) (x : def term)
  := max (depth (dtype x)) (depth (dbody x)).

Definition list_depth_gen {A} (depth : A nat) :=
  fix list_depth (l : list A) : nat :=
    match l with
    | [] ⇒ 0
    | a :: v ⇒ (max (depth a) (list_depth v))
    end.

Definition mfixpoint_depth_gen (depth : term nat) (l : mfixpoint term) :=
  list_depth_gen (def_depth_gen depth) l.

Definition decl_depth_gen (depth : term nat) (x : context_decl) :=
  max (depth (decl_type x)) (option_default depth (decl_body x) 0).

Definition context_depth_gen (depth : term nat) (l : context) :=
  list_depth_gen (decl_depth_gen depth) l.

Definition branch_depth_gen (depth : term nat) p (br : branch term) :=
  let pard := list_depth_gen depth p.(pparams) in
  let bctxd := context_depth_gen depth br.(bcontext) in
  max (pard + bctxd) (depth br.(bbody)).

Definition predicate_depth_gen (depth : term nat) (p : PCUICAst.predicate term) :=
  let pard := list_depth_gen depth p.(pparams) in
  let pctxd := context_depth_gen depth p.(pcontext) in
    max (pard + pctxd) (depth p.(preturn)).

Fixpoint depth t : nat :=
  match t with
  | tRel i ⇒ 1
  | tEvar ev argsS (list_depth_gen depth args)
  | tLambda na T MS (max (depth T) (depth M))
  | tApp u vS (max (depth u) (depth v))
  | tProd na A BS (max (depth A) (depth B))
  | tLetIn na b t b'S (max (depth b) (max (depth t) (depth b')))
  | tCase ind p c brsS (max (predicate_depth_gen depth p)
    (max (depth c) (list_depth_gen (branch_depth_gen depth p) brs)))
  | tProj p cS (depth c)
  | tFix mfix idxS (mfixpoint_depth_gen depth mfix)
  | tCoFix mfix idxS (mfixpoint_depth_gen depth mfix)
  | _ ⇒ 1
  end.

Notation context_depth := (context_depth_gen depth).
Notation list_depth := (list_depth_gen depth).
Notation mfixpoint_depth := (mfixpoint_depth_gen depth).

Lemma depth_mkApps f l : max (depth f) (list_depth l) depth (mkApps f l).
Proof.
  induction l in f |- *; simpl; try lia.
  specialize (IHl (tApp f a)).
  cbn -[max] in IHl.
  etransitivity; tea.
  lia.
Qed.

Lemma mfixpoint_depth_In {mfix d} :
  In d mfix
  depth (dbody d) mfixpoint_depth mfix
  depth (dtype d) mfixpoint_depth mfix.
Proof.
  induction mfix in d |- *; simpl; auto.
  move⇒ [->|H]. unfold def_depth_gen. split; try lia.
  destruct (IHmfix d H). split; lia.
Qed.

Lemma mfixpoint_depth_nth_error {mfix i d} :
  nth_error mfix i = Some d
  depth (dbody d) mfixpoint_depth mfix.
Proof.
  induction mfix in i, d |- *; destruct i; simpl; try congruence.
  move⇒ [] →. unfold def_depth_gen. lia.
  move/IHmfix. lia.
Qed.

Lemma nth_error_depth {A} (f : A nat) {l : list A} {n x} :
  nth_error l n = Some x
  f x list_depth_gen f l.
Proof.
  induction l in n |- *; destruct n; simpl ⇒ //; auto.
  - intros [= <-]. lia.
  - intros hnth. specialize (IHl _ hnth). lia.
Qed.

Lemma map_depth_hom {A} {depth : A nat} {l : list A} {f : A A} :
  ( x : A, depth (f x) = depth x)
  list_depth_gen depth (map f l) = list_depth_gen depth l.
Proof.
  intros Hf.
  revert l.
  fix aux 1. destruct l. simpl; auto. simpl.
  f_equal. apply Hf. apply aux.
Defined.

Lemma depth_lift n k t : depth (lift n k t) = depth t.
Proof.
  revert n k t.
  fix aux 3.
  destruct t; simpl; try rewrite map_depth_hom; try lia.
  all:try now rewrite !aux.
  all:try intros; auto.
  - destruct x. simpl. unfold branch_depth_gen; cbn.
    f_equal. apply aux.
  - f_equal. f_equal.
    rewrite /predicate_depth_gen /=. f_equal.
    f_equal. exact (map_depth_hom (aux n k)).
    apply aux.
    f_equal. apply aux.
    revert brs.
    fix aux' 1. destruct brs; simpl; trivial.
    f_equal. 2:apply aux'.
    rewrite /branch_depth_gen /=.
    f_equal. f_equal. apply (map_depth_hom (aux n k)).
  - unfold mfixpoint_depth_gen.
    f_equal.
    apply map_depth_hom. intros.
    simpl. destruct x. simpl. unfold def_depth_gen. simpl.
    f_equal; apply aux.
  - unfold mfixpoint_depth_gen.
    f_equal.
    apply map_depth_hom. intros.
    simpl. destruct x. simpl. unfold def_depth_gen. simpl.
    f_equal; apply aux.
Qed.

Lemma All_depth {s l} k :
  All (fun x k, depth (subst s k x) depth x + list_depth s) l
  list_depth (map (subst s k) l) list_depth l + list_depth s.
Proof.
  intros a. revert k. induction a; simpl; auto; intros; try lia.
  specialize (p k); specialize (IHa k). lia.
Qed.

Lemma depth_subst s k t : depth (subst s k t) depth t + list_depth s.
Proof.
  induction t in k |- × using term_forall_list_ind; simpl; auto; try lia.
  - destruct Nat.leb. destruct nth_error eqn:hnth.
    eapply (nth_error_depth depth) in hnth.
    rewrite depth_lift. lia. simpl. lia.
    simpl. lia.
  - eapply (All_depth k) in X. lia.
  - specialize (IHt1 k); specialize (IHt2 (S k)); lia.
  - specialize (IHt1 k); specialize (IHt2 (S k)); lia.
  - specialize (IHt1 k); specialize (IHt2 k); specialize (IHt3 (S k)); lia.
  - specialize (IHt1 k); specialize (IHt2 k); lia.
  - destruct X as [? [? ?]].
    rewrite /predicate_depth_gen /=.
    eapply (All_depth k) in a.
    assert ((list_depth (map (subst s k) (pparams p)) +
        context_depth (pcontext p))
      (list_depth (pparams p) + context_depth (pcontext p) + list_depth s)) by lia.
    specialize (IHt k).
    assert (list_depth_gen (branch_depth_gen depth (map_predicate_k id (subst s) k p)) (map_branches_k (subst s) id k l)
        (list_depth_gen (branch_depth_gen depth p) l) + list_depth s).
    { clear -a X0 k. induction X0; simpl; auto; try lia.
      destruct p0. specialize (l0 (#|bcontext x| + k)).
      rewrite {1 3}/branch_depth_gen /= /id. rewrite /id in IHX0. lia. }
    specialize (l0 (#|pcontext p| + k)).
    assert ((list_depth (map (subst s k) (pparams p)) + context_depth (pcontext p))
      (list_depth (pparams p) + context_depth (pcontext p) + list_depth s)) by lia.
    lia.
  - specialize (IHt k). lia.
  - rewrite /mfixpoint_depth_gen. generalize #|m|.
    induction X in k |- *; simpl; auto; try lia.
    destruct p. intros n'.
    rewrite {1 3}/def_depth_gen /=.
    specialize (l0 k).
    specialize (l1 (n' + k)). simpl in l1.
    specialize (IHX k n'). lia.
  - rewrite /mfixpoint_depth_gen. generalize #|m|.
    induction X in k |- *; simpl; auto; try lia.
    destruct p. intros n'.
    rewrite {1 3}/def_depth_gen /=.
    specialize (l0 k).
    specialize (l1 (n' + k)). simpl in l1.
    specialize (IHX k n'). lia.
Qed.

Lemma depth_subst_instance u t : depth (subst_instance u t) = depth t.
Proof.
  revert t.
  fix aux 1.
  destruct t; simpl; try rewrite map_depth_hom; try lia; tas.
  all:try rewrite !aux //.
  - destruct x. simpl. unfold branch_depth_gen; cbn.
    f_equal. apply aux.
  - f_equal. f_equal.
    rewrite /predicate_depth_gen /=. f_equal.
    f_equal. exact (map_depth_hom aux).
    apply aux.
    f_equal. rewrite /branch_depth_gen /=.
    revert brs.
    fix aux' 1. destruct brs; simpl; auto.
    f_equal; auto. f_equal. f_equal. exact (map_depth_hom aux).
  - unfold mfixpoint_depth_gen.
    f_equal.
    apply map_depth_hom. intros.
    simpl. destruct x. simpl. unfold def_depth_gen. simpl.
    f_equal; apply aux.
  - unfold mfixpoint_depth_gen.
    f_equal.
    apply map_depth_hom. intros.
    simpl. destruct x. simpl. unfold def_depth_gen. simpl.
    f_equal; apply aux.
Qed.

Lemma depth_subst_decl s k d :
  decl_depth_gen depth (subst_decl s k d) decl_depth_gen depth d + list_depth s.
Proof.
  destruct d as [na [b|] ty]; rewrite /decl_depth_gen /=.
  pose proof (depth_subst s k ty).
  pose proof (depth_subst s k b). lia.
  pose proof (depth_subst s k ty). lia.
Qed.

Lemma depth_subst_context s k ctx :
  context_depth (subst_context s k ctx) context_depth ctx + list_depth s.
Proof.
  induction ctx; simpl; try lia.
  rewrite subst_context_snoc /=.
  pose proof (depth_subst_decl s (#|ctx| + k) a). lia.
Qed.

Lemma depth_subst_instance_context u (ctx : context) : context_depth (subst_instance u ctx) = context_depth ctx.
Proof.
  induction ctx; simpl; auto.
  rewrite IHctx. f_equal.
  rewrite /decl_depth_gen /=.
  destruct decl_body; rewrite /= !depth_subst_instance //.
Qed.


Definition onctx_rel (P : context term Type) (Γ Δ : context) :=
  All_local_env (PCUICInduction.on_local_decl (fun ΔP (Γ ,,, Δ))) Δ.

Definition CasePredProp (P : context term Type) Γ (p : predicate term) :=
  All (P Γ) p.(pparams) × onctx_rel P Γ (inst_case_context p.(pparams) p.(puinst) p.(pcontext)) ×
  P (Γ ,,, inst_case_context p.(pparams) p.(puinst) p.(pcontext)) p.(preturn).

Definition CaseBrsProp p P Γ (brs : list (branch term)) :=
  All (fun x : branch termonctx_rel P Γ (inst_case_context p.(pparams) p.(puinst) x.(bcontext))
     × P (Γ ,,, inst_case_context p.(pparams) p.(puinst) x.(bcontext)) (bbody x)) brs.

Lemma list_depth_app {A} (depth : A nat) (l l' : list A) :
  list_depth_gen depth (l ++ l') = max (list_depth_gen depth l) (list_depth_gen depth l').
Proof.
  induction l; simpl; auto.
  rewrite IHl. lia.
Qed.

Lemma In_list_depth {A : Type} (f : A nat) :
   x xs, In x xs f x < S (list_depth_gen f xs).
Proof.
  intros. induction xs.
  destruct H.
  × destruct H. simpl; subst. lia.
    specialize (IHxs H). simpl. lia.
Qed.

Lemma list_depth_rev {A} (depth : A nat) (l : list A) :
  list_depth_gen depth (rev l) = list_depth_gen depth l.
Proof.
  induction l using rev_ind; simpl; auto; try lia.
  rewrite rev_app_distr /= list_depth_app /=. lia.
Qed.

Lemma list_depth_mapi_rec_le {A B} (l : list A) (f : nat A B) k
  (depthA : A nat) (depthB : B nat) :
  ( i x, depthB (f i x) depthA x)
  list_depth_gen depthB (mapi_rec f l k) list_depth_gen depthA l.
Proof.
  intro H. induction l in k |- ×. reflexivity.
  simpl. specialize (H k a). specialize (IHl (S k)). lia.
Qed.

Lemma context_depth_inst_case_context pars puinst pctx :
  context_depth (inst_case_context pars puinst pctx)
  context_depth pctx + list_depth pars.
Proof.
  rewrite /inst_case_context.
  rewrite -list_depth_rev.
  etransitivity; [eapply depth_subst_context|].
  now rewrite depth_subst_instance_context.
Qed.

Lemma term_forall_ctx_list_ind :
   (P : context term Type),
    ( Γ (n : nat), P Γ (tRel n))
    ( Γ (i : ident), P Γ (tVar i))
    ( Γ (n : nat) (l : list term), All (P Γ) l P Γ (tEvar n l))
    ( Γ s, P Γ (tSort s))
    ( Γ (n : aname) (t : term), P Γ t t0 : term, P (vass n t :: Γ) t0 P Γ (tProd n t t0))
    ( Γ (n : aname) (t : term), P Γ t t0 : term, P (vass n t :: Γ) t0 P Γ (tLambda n t t0))
    ( Γ (n : aname) (t : term),
        P Γ t t0 : term, P Γ t0 t1 : term, P (vdef n t t0 :: Γ) t1 P Γ (tLetIn n t t0 t1))
    ( Γ (t u : term),
      ( t', depth t' < depth (tApp t u) P Γ t')
      P Γ t P Γ u P Γ (tApp t u))
    ( Γ s (u : list Level.t), P Γ (tConst s u))
    ( Γ (i : inductive) (u : list Level.t), P Γ (tInd i u))
    ( Γ (i : inductive) (n : nat) (u : list Level.t), P Γ (tConstruct i n u))
    ( Γ (ci : case_info) (p : predicate term) (t : term) (brs : list (branch term)),
        CasePredProp P Γ p
        P Γ t
        CaseBrsProp p P Γ brs
        P Γ (tCase ci p t brs))
    ( Γ (s : projection) (t : term), P Γ t P Γ (tProj s t))
    ( Γ (m : mfixpoint term) (n : nat),
        All_local_env (PCUICInduction.on_local_decl (fun Γ' tP (Γ ,,, Γ') t)) (fix_context m)
        tFixProp (P Γ) (P (Γ ,,, fix_context m)) m P Γ (tFix m n))
    ( Γ (m : mfixpoint term) (n : nat),
        All_local_env (PCUICInduction.on_local_decl (fun Γ' tP (Γ ,,, Γ') t)) (fix_context m)
        tFixProp (P Γ) (P (Γ ,,, fix_context m)) m P Γ (tCoFix m n))
    
     Γ (t : term), P Γ t.
Proof.
  intros ???????????????? Γ t.
  revert Γ t. set(foo:=CoreTactics.the_end_of_the_section). intros.
  Subterm.rec_wf_rel aux t (MR lt depth); unfold MR in *; simpl. clear H1.
  assert (auxl : Γ {A} (l : list A) (f : A term),
    list_depth_gen (fun xdepth (f x)) l < depth pr0
    All (fun xP Γ (f x)) l).
  { induction l; try solve [constructor].
    movef /= Hdepth.
    constructor.
    × eapply aux ⇒ //. red. lia.
    × apply IHl ⇒ //. lia. }
  assert ( mfix, context_depth (fix_context mfix) mfixpoint_depth_gen depth mfix).
  { induction mfix. simpl. auto. simpl. unfold fix_context.
    unfold context_depth.
    rewrite /context_depth list_depth_rev /=. cbn.
    rewrite depth_lift. unfold context_depth in IHmfix.
    epose (list_depth_mapi_rec_le mfix
                                 (fun (i : nat) (d : def term) ⇒ vass (dname d) ((lift0 i) (dtype d))) 1
                                 (def_depth_gen depth) (decl_depth_gen depth)).
    forward l. intros. destruct x; cbn; rewrite depth_lift. lia.
    rewrite /mfixpoint_depth_gen {1}/def_depth_gen. lia. }
  assert (auxΓ : Γ Δ,
             context_depth Δ < depth pr0
             onctx_rel P Γ Δ).
  { moveΓ Δ.
    induction Δ; cbn.
    - constructor.
    - case: a ⇒ [na [b|] ty] /=;
      rewrite {1}/decl_depth_gen /context_depth_gen /= ⇒ Hlt; constructor; auto.
      + eapply IHΔ ⇒ //. unfold context_depth. lia.
      + simpl. apply aux ⇒ //. red. lia.
      + simpl. split.
        × apply aux ⇒ //. red. lia.
        × apply aux⇒ //; red; lia.
      + apply IHΔ ⇒ //; unfold context_depth; lia.
      + apply aux ⇒ //. red. lia. }
  assert ( m, list_depth_gen (fun x : def termdepth (dtype x)) m < S (mfixpoint_depth_gen depth m)).
  { clear. unfold mfixpoint_depth_gen, def_depth_gen. induction m. simpl. auto. simpl. lia. }
  assert ( m, list_depth_gen (fun x : def termdepth (dbody x)) m < S (mfixpoint_depth_gen depth m)).
  { clear. unfold mfixpoint_depth_gen, def_depth_gen. induction m. simpl. auto. simpl. lia. }

  move aux at top. move auxl at top. move auxΓ at top.

  destruct pr0; eauto;
    (move: pr2⇒ /= /and3P [pr20 pr21 pr22] || move: pr2 ⇒ /= /andP [pr20 pr21] || idtac);
    try match reverse goal with
          |- context [tFix _ _] ⇒ idtac
        | H : _ |- _solve [apply H; (eapply aux || eapply auxl); auto; red; simpl; try lia]
        end.

  - eapply X10; eauto.
    × red. split.
      + eapply auxl; auto. simpl. unfold predicate_depth_gen, branch_depth_gen.
        now change (fun xdepth x) with depth; lia.
      + split.
        ++ apply auxΓ. simpl. unfold predicate_depth_gen.
          pose proof (context_depth_inst_case_context p.(pparams) p.(puinst) p.(pcontext)). lia.
        ++ eapply aux; auto. simpl. unfold predicate_depth_gen. lia.
    × eapply aux ⇒ //. simpl; lia.
    × red. simpl in aux.
      have auxbr := fun Γ t (H : depth t list_depth_gen (branch_depth_gen depth p) brs) ⇒
        aux Γ t ltac:(lia).
      move: auxbr.
      clear -auxΓ.
      induction brs. simpl. constructor.
      constructor. simpl in auxbr.
      + split. eapply auxΓ. simpl.
        unfold branch_depth_gen at 1. rewrite /predicate_depth_gen /=.
        pose proof (context_depth_inst_case_context p.(pparams) p.(puinst) a.(bcontext)).
        lia.
        eapply auxbr. unfold branch_depth_gen. lia.
      + eapply IHbrs. intros. apply auxΓ. simpl in ×. lia.
        intros. apply auxbr. simpl. lia.
  - eapply X12; try (apply aux; red; simpl; lia).
    apply auxΓ ⇒ //. simpl. specialize (H mfix). lia.
    red. apply All_pair. split; apply auxl; simpl; auto.

  - eapply X13; try (apply aux; red; simpl; lia).
    apply auxΓ ⇒ //. simpl. specialize (H mfix). lia.
    red. apply All_pair. split; apply auxl; simpl; auto.
Defined.

Definition CasePredProp_depth (P : term Type) (p : predicate term) :=
  All P p.(pparams) × onctx P (inst_case_context p.(pparams) p.(puinst) p.(pcontext)) ×
  P p.(preturn).

Definition CaseBrsProp_depth p (P : term Type) (brs : list (branch term)) :=
  All (fun x : branch termonctx P (inst_case_context p.(pparams) p.(puinst) x.(bcontext))
     × P (bbody x)) brs.

Lemma term_ind_depth_app :
   (P : term Type),
    ( (n : nat), P (tRel n))
    ( (i : ident), P (tVar i))
    ( (n : nat) (l : list term), All (P) l P (tEvar n l))
    ( s, P (tSort s))
    ( (n : aname) (t : term), P t t0 : term, P t0 P (tProd n t t0))
    ( (n : aname) (t : term), P t t0 : term, P t0 P (tLambda n t t0))
    ( (n : aname) (t : term),
        P t t0 : term, P t0 t1 : term, P t1 P (tLetIn n t t0 t1))
    ( (t u : term),
      ( t', depth t' < depth (tApp t u) P t')
      P t P u P (tApp t u))
    ( s (u : list Level.t), P (tConst s u))
    ( (i : inductive) (u : list Level.t), P (tInd i u))
    ( (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u))
    ( (ci : case_info) (p : predicate term) (t : term) (brs : list (branch term)),
        CasePredProp_depth P p
        P t
        CaseBrsProp_depth p P brs
        P (tCase ci p t brs))
    ( (s : projection) (t : term), P t P (tProj s t))
    ( (m : mfixpoint term) (n : nat),
        onctx P (fix_context m)
        tFixProp P P m P (tFix m n))
    ( (m : mfixpoint term) (n : nat),
        onctx P (fix_context m)
        tFixProp P P m P (tCoFix m n))
    
     (t : term), P t.
Proof.
  intros ???????????????? t.
  revert t. set(foo:=CoreTactics.the_end_of_the_section). intros.
  Subterm.rec_wf_rel aux t (MR lt depth); unfold MR in *; simpl. clear H0.
  assert (auxl : {A} (l : list A) (f : A term),
    list_depth_gen (fun xdepth (f x)) l < depth pr1
    All (fun xP (f x)) l).
  { induction l; try solve [constructor].
    movef /= Hdepth.
    constructor.
    × eapply aux ⇒ //. red. lia.
    × apply IHl ⇒ //. lia. }
  assert ( mfix, context_depth (fix_context mfix) mfixpoint_depth_gen depth mfix).
  { induction mfix. simpl. auto. simpl. unfold fix_context.
    unfold context_depth.
    rewrite /context_depth list_depth_rev /=. cbn.
    rewrite depth_lift. unfold context_depth in IHmfix.
    epose (list_depth_mapi_rec_le mfix
                                 (fun (i : nat) (d : def term) ⇒ vass (dname d) ((lift0 i) (dtype d))) 1
                                 (def_depth_gen depth) (decl_depth_gen depth)).
    forward l. intros. destruct x; cbn; rewrite depth_lift. lia.
    rewrite /mfixpoint_depth_gen {1}/def_depth_gen. lia. }
  assert (auxΓ : Δ,
             context_depth Δ < depth pr1
             onctx P Δ).
  { moveΓ h.
    induction Γ; cbn.
    - constructor.
    - case: a h ⇒ [na [b|] ty] /=;
      rewrite {1}/decl_depth_gen /context_depth_gen /= ⇒ Hlt; constructor; auto.
      + simpl. split.
        × apply aux ⇒ //. red. cbn. lia.
        × apply aux⇒ //; red; lia.
      + apply IHΓ ⇒ //; unfold context_depth; lia.
      + red; cbn. split. apply aux ⇒ //. red. lia. exact tt.
      + apply IHΓ ⇒ //. unfold context_depth; lia. }
  assert ( m, list_depth_gen (fun x : def termdepth (dtype x)) m < S (mfixpoint_depth_gen depth m)).
  { clear. unfold mfixpoint_depth_gen, def_depth_gen. induction m. simpl. auto. simpl. lia. }
  assert ( m, list_depth_gen (fun x : def termdepth (dbody x)) m < S (mfixpoint_depth_gen depth m)).
  { clear. unfold mfixpoint_depth_gen, def_depth_gen. induction m. simpl. auto. simpl. lia. }

  move aux at top. move auxl at top. move auxΓ at top.

  destruct pr1; eauto;
    (move: pr2⇒ /= /and3P [pr20 pr21 pr22] || move: pr2 ⇒ /= /andP [pr20 pr21] || idtac);
    try match reverse goal with
          |- context [tFix _ _] ⇒ idtac
        | H : _ |- _solve [apply H; (eapply aux || eapply auxl); auto; red; simpl; try lia]
        end.

  - eapply X10; eauto.
    × red. split.
      + eapply auxl; auto. simpl. unfold predicate_depth_gen, branch_depth_gen.
        now change (fun xdepth x) with depth; lia.
      + split.
        ++ apply auxΓ. simpl. unfold predicate_depth_gen.
          pose proof (context_depth_inst_case_context p.(pparams) p.(puinst) p.(pcontext)). lia.
        ++ eapply aux; auto. simpl. unfold predicate_depth_gen. lia.
    × eapply aux ⇒ //. simpl; lia.
    × red. simpl in aux.
      have auxbr := fun t (H : depth t list_depth_gen (branch_depth_gen depth p) brs) ⇒
        aux t ltac:(lia).
      move: auxbr.
      clear -auxΓ.
      induction brs. simpl. constructor.
      constructor. simpl in auxbr.
      + split. eapply auxΓ. simpl.
        unfold branch_depth_gen at 1. rewrite /predicate_depth_gen /=.
        pose proof (context_depth_inst_case_context p.(pparams) p.(puinst) a.(bcontext)).
        lia.
        eapply auxbr. unfold branch_depth_gen. lia.
      + eapply IHbrs. intros. apply auxΓ. simpl in ×. lia.
        intros. apply auxbr. simpl. lia.
  - eapply X12; try (apply aux; red; simpl; lia).
    apply auxΓ ⇒ //. simpl. specialize (H mfix). lia.
    red. apply All_pair. split; apply auxl; simpl; auto.

  - eapply X13; try (apply aux; red; simpl; lia).
    apply auxΓ ⇒ //. simpl. specialize (H mfix). lia.
    red. apply All_pair. split; apply auxl; simpl; auto.
Defined.