proposition: Lemma hereditary_subst_type Γ Γ' t T u U : Γ |-- u : U -> Γ' @ (U :: Γ) |-- t : T -> let (t', o) := hereditary_subst (U, u, t) (length Γ') in (Γ' @ Γ |-- t' : T /\ (forall ty prf, o = Some (exist ty prf) -> ty = T)).
proof: Proof. intros. funelim (hereditary_subst (U, u, t) (length Γ')); DepElim.simpl_dep_elim; subst; try (split; [ (intros; try discriminate) | solve [ intros; discriminate ] ]); DepElim.simplify_dep_elim. invert_term. simpl in *. apply abstraction. specialize (H Γ (A0 :: Γ')). simpl in H. eqns_specialize_eqs H. simpl in H. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). specialize (H _ H0 H1). apply H; auto. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). depelim H2. constructor. now apply H. now apply H0. depelim H0. term. simpl. apply Nat.compare_eq in Heq; subst. depelim H0. rewrite !nth_length. split. term. intros. noconf H1. auto. apply Nat.compare_lt_iff in Heq. depelim H0. replace (nth i (Γ' @ (_ :: Γ)) unit) with (nth i (Γ' @ Γ) unit). constructor. rewrite app_length. auto with arith. now do 2 rewrite <- nth_extend_right by auto. pose (substitutive _ _ _ _ _ _ H0 H). simp subst in t. rewrite Heq in t. simp subst in t. simpl in *. - on_call (hereditary_subst (A, a, arg)) ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in *). on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ). dependent elimination H2 as [application _ U T f arg tyfn tyu]. specialize (H _ _ H1 tyu). specialize (Hind _ _ H1 tyfn). rewrite Heq in Hind. destruct Hind as [Ht' Ht'']. dependent elimination Ht' as [abstraction _ U T abs tyabs]. eqns_specialize_eqs Ht''. noconf Ht''. destruct H as [Ht tty]. specialize (H0 _ [] _ _ _ _ Ht tyabs eq_refl). destruct H0 as [H0 H5]. split; auto. intros ty prf0 Heq'. noconf Heq'. auto. - apply is_lambda_inr in Heq. revert Heq. intros <-. depelim H1. specialize (H _ _ H0 H1_0). specialize (Hind _ _ H0 H1_). on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ). on_call (hereditary_subst (A, a, arg)) ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ). destruct H, Hind. econstructor; eauto. - simpl in *. depelim H0. specialize (Hind _ _ H H0). rewrite Heq in Hind. destruct Hind. depelim H1. intuition auto. eqns_specialize_eqs H2. noconf H2. now noconf H1. - apply is_pair_inr in Heq. revert Heq. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ). depelim H0. intros <-. specialize (Hind _ _ H H0); eauto. destruct Hind. now apply pair_elim_fst with B. - simpl. depelim H0. specialize (Hind _ _ H H0). rewrite Heq in Hind. destruct Hind. depelim H1. intuition auto. eqns_specialize_eqs H2. noconf H2. now noconf H1. - apply is_pair_inr in Heq. revert Heq. on_call hereditary_subst ltac:(fun c => remember c as hsubst; destruct hsubst; simpl in * ). intros Ht2; subst t. simpl in *. depelim H0. specialize (Hind _ _ H H0); eauto. now apply pair_elim_snd with A0. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat