proposition: Lemma hereditary_subst_subst U u t Γ' : (forall Γ T, Γ |-- u <= U -> match hereditary_subst (U, u, t) (length Γ') with | (t', Some (exist ty _)) => ((Γ' @ (U :: Γ) |-- t <= T -> Γ' @ Γ |-- t' <= T /\ ty = T) /\ (Γ' @ (U :: Γ) |-- t => T -> Γ' @ Γ |-- t' <= T /\ ty = T)) | (t', None) => (Γ' @ (U :: Γ) |-- t <= T -> Γ' @ Γ |-- t' <= T) /\ (Γ' @ (U :: Γ) |-- t => T -> Γ' @ Γ |-- t' => T) end).
proof: Proof. funelim (hereditary_subst (U, u, t) (length Γ')); simpl in *. let Hind := fresh "Hind" in rename H into Hind; intros ?? Hu. simpl. simpl in *. - on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). split; intros Hsyn; [| elim (synth_arrow False Hsyn)]. invert_term. constructor. specialize (Hind _ _ _ (A0 :: Γ') eq_refl). simpl in *. specialize (Hind _ B Hu). destruct o as [[ty prf]|], Hind as [Hind0 Hind1]. apply Hind0; eauto. eauto. elim (synth_arrow False H0). - do 2 on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). split; intros Hsyn; [|elim (synth_pair False Hsyn)]. invert_term. specialize (H0 _ B H1). specialize (H _ A0 H1). destruct o as [[ty prf]|], o0 as [[ty' prf']|], H, H0; destruct_conjs; constructor; eauto. now apply H. now apply H0. now apply H. now apply H0. elim (synth_pair False H3). - split; intros Hsyn; [|elim (synth_unit False Hsyn)]. depelim Hsyn. term. elim (synth_unit False H1). - apply Nat.compare_eq in Heq; subst i. split; intros Hsyn; depelim Hsyn; rewrite ?nth_length. depelim H1; rewrite !nth_length. now split; term. split; term. - apply Nat.compare_lt_iff in Heq. split; intros Hsyn; depelim Hsyn; [depelim H1;constructor;auto|]; (rewrite nth_app_l by lia; rewrite <- nth_app_l with (l':=Γ) by lia; constructor; rewrite app_length; auto with arith). - apply Nat.compare_gt_iff in Heq. split; intros Hsyn; depelim Hsyn. depelim H1. constructor. auto. replace (nth i (Γ' @ (A :: Γ)) unit) with (nth (pred i) (Γ' @ Γ) unit). constructor. rewrite app_length in *. simpl in H1. lia. now apply nth_pred. replace (nth _ (Γ' @ (_ :: _)) unit) with (nth (pred i) (Γ' @ Γ) unit). constructor. rewrite app_length in *. simpl in H0. lia. now apply nth_pred. - cbn. on_call (hereditary_subst (A,a,arg)) ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). specialize (H0 _ _ _ [] eq_refl). rewrite Heq in Hind. revert H0. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). intros. assert((Γ' @ (A :: Γ) |-- @(f, arg) => T → Γ' @ Γ |-- t0 <= T ∧ B' = T)). intros Ht; depelim Ht. destruct (Hind Γ (A0 ---> T) H1). specialize (H _ A' H1). destruct (H4 Ht). noconf H6. depelim H5. split; auto. destruct o; try destruct h; destruct H. destruct (H H2). subst x. specialize (H0 _ B' H7). destruct o0 as [[ty typrf]|]; destruct H0 as [Hcheck Hinf]. now apply Hcheck. now apply Hcheck. specialize (H0 _ B' (H H2)). destruct o0 as [[ty typrf]|]; destruct H0 as [Hcheck Hinf]. now apply Hcheck. now apply Hcheck. split; auto. depelim H6. split; eauto. intros Ht3u; apply H2. now depelim Ht3u. - intros Γ T Hu. assert(Γ' @ (A :: Γ) |-- @( f, arg) => T → Γ' @ Γ |-- @( f', fst (hereditary_subst (A, a, arg) (length Γ'))) => T). intros Ht; depelim Ht. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). revert Heq. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). intros. pose (Hind _ (A0 ---> T) Hu). destruct o0 as [[ty prf']|]. + destruct y as [Hind' Hind'']. specialize (Hind'' Ht). destruct Hind''; subst ty. specialize (H _ A0 Hu). destruct o as [[ty' prf'']|]. ++ destruct H as [Hind0 Hind0']. specialize (Hind0 H0). destruct Hind0. subst ty'. eapply application_synth; eauto. simpl in *. depelim H1. simp is_lambda in Heq. noconf Heq. depelim H1. ++ depelim H1. simp is_lambda in Heq. noconf Heq. depelim H1. + clear y. specialize (H _ A0 Hu). destruct (Hind _ (A0 ---> T) Hu). apply is_lambda_inr in Heq. cbn in Heq; subst t0. simpl. destruct o as [[ty prf]|]; destruct H as [Hindt0 Hindt0']. eapply application_synth; eauto. now apply Hindt0. eapply application_synth; eauto. + split; auto. intros H2. depelim H2. constructor; auto. - simpl in Heq. autorewrite with is_pair in Heq. simpl in prf. intros Γ T Hu. assert( (Γ' @ (A :: Γ) |-- Fst t' => T → Γ' @ Γ |-- u <= T ∧ a' = T)). intros Ht; depelim Ht. specialize (Hind _ (T × B) Hu). revert Hind. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). noconf Heq. intros [Hind Hind']. specialize (Hind' Ht). destruct Hind' as [H0 H1]. noconf H1. depelim H0. split; auto. depelim H0. split; auto. intros H1. depelim H1. intuition. - intros Γ T Hu. assert (Γ' @ (A :: Γ) |-- Fst t' => T → Γ' @ Γ |-- Fst p' => T). intros Ht; depelim Ht. specialize (Hind _ (T × B) Hu). revert Hind. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). destruct o as [[ty prf]|]. intros [Hind Hind']. destruct (Hind' Ht). subst ty. depelim H. simp is_pair in Heq. discriminate. depelim H. apply is_pair_inr in Heq. simpl in Heq ; subst p'. intros [Hind Hind']. eapply pair_elim_fst_synth. now apply Hind'. split; auto. intros H2. depelim H2. intuition auto with term. - intros Γ T Hu. assert((Γ' @ (A :: Γ) |-- Snd t' => T → Γ' @ Γ |-- v <= T ∧ b' = T)). intros Ht; depelim Ht. specialize (Hind _ (A0 × T) Hu). revert Hind. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). noconf Heq. intros [Hind Hind']. specialize (Hind' Ht). destruct Hind' as [H0 H1]. noconf H1. depelim H0. split; auto. depelim H0. split; auto. intros H1. depelim H1. intuition auto with term. - intros Γ T Hu. assert (Γ' @ (A :: Γ) |-- Snd t' => T → Γ' @ Γ |-- Snd p' => T). intros Ht; depelim Ht. specialize (Hind _ (A0 × T) Hu). revert Hind. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). destruct o as [[ty prf]|]. intros [Hind Hind']. destruct (Hind' Ht). subst ty. depelim H. simp is_pair in Heq. discriminate. depelim H. intros [Hind Hind']. apply is_pair_inr in Heq. subst p'. simpl in *. specialize (Hind' Ht). econstructor; eauto. split; auto. intros H1. depelim H1. term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat