proposition: Lemma enc_term_app sigma s: (forall x, x ∈ consts s -> R' x = None -> x ∈ C) -> inv_term C (sigma • enc_term C s) >* inv_subst C sigma • s.
proof: Proof. Proof using n. intros H. unfold enc_term, inv_term. asimpl. rewrite subst_consts_Lambda. rewrite AppR_Lambda'; simplify; trivial. replace (ι >> _) with ι by (fext; intros ?; reflexivity). pose (theta x := AppR (subst_consts ι (ren (plus (length C)) (sigma x))) (map var (nats (length C)))). erewrite subst_consts_subst with (kappa := enc_const C) (theta := theta). - rewrite subst_consts_comp. rewrite subst_consts_subst with (kappa := const) (theta := inv_subst C sigma) . rewrite subst_consts_ident; auto. + intros x V. unfold theta, inv_subst. rewrite subst_consts_AppR, subst_consts_comp. rewrite map_id_list. 2: intros ??; mapinj; reflexivity. rewrite subst_consts_ident; trivial. replace (ι >> _) with (ι >> ren (plus (length C))). 2: fext; intros c; unfold funcomp, enc_const, R'; cbn; now rewrite tight_retr. rewrite ren_subst_consts_commute. unfold inv_term. asimpl. eapply refl_star. f_equal. * eapply idSubst_exp. intros y; unfold funcomp. erewrite sapp_ge_in; simplify; auto. * clear theta V. eapply list_pointwise_eq. intros m; rewrite !nth_error_map_option. destruct (le_lt_dec (length C) m) as [H1|H1]. -- edestruct nth_error_None as [_ ->]. edestruct nth_error_None as [_ ->]. all: cbn; simplify; auto. -- rewrite nth_nats; trivial; cbn. destruct (nth_error_lt_Some _ m C) as [c H3]; trivial. rewrite H3; cbn. erewrite nth_error_sapp; trivial. erewrite map_nth_error; auto. + intros ??. unfold funcomp. unfold enc_const. destruct (R' x) eqn: ?. cbn. eapply tight_is_tight in Heqo; now subst. eapply H in H0; trivial. eapply find_in in H0 as [m H0]; rewrite H0. cbn. erewrite nth_error_sapp; trivial. erewrite map_nth_error; trivial. eapply find_Some; auto. - intros; unfold enc_var, theta. rewrite subst_consts_AppR; cbn. rewrite AppR_subst; cbn; rewrite it_up_ge; trivial; simplify. rewrite subst_consts_AppR, subst_consts_comp, subst_consts_ident. 2: intros ?; unfold funcomp, enc_const, R'; cbn; now rewrite tight_retr. eapply refl_star. f_equal. rewrite map_id_list; trivial. intros ??; mapinj; mapinj; cbn. rewrite it_up_lt; auto using nats_lt. - intros. unfold enc_const. destruct (R' x) eqn: ?. cbn. eapply tight_is_tight in Heqo; now subst. eapply H in H0; trivial. eapply find_in in H0 as [m H0]; rewrite H0. eapply find_Some, nth_error_Some_lt in H0. cbn; erewrite it_up_lt; auto. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)