proposition: Lemma enc_subst_term_reduce tau s: (forall x c, c ∈ consts (tau x) -> R' c = None -> c ∈ C) -> (forall x, x ∈ consts s -> R' x = None -> x ∈ C) -> enc_subst C tau • enc_term C s >* enc_term C (tau • s).
proof: Proof. Proof using n. intros H1 H2; unfold enc_term. asimpl. eapply Lambda_steps_proper. rewrite subst_consts_subst; trivial. - intros x ?. unfold funcomp at 1. unfold enc_var. rewrite !subst_consts_AppR, AppR_subst; cbn. rewrite it_up_ge; simplify; trivial. rewrite map_id_list; cbn. rewrite map_map; cbn. change (fun x => @var Y x) with (@var Y). unfold enc_subst at 1, enc_term. rewrite Lambda_ren. rewrite AppR_Lambda'; simplify; trivial. asimpl. rewrite subst_consts_subst; trivial. + intros ? ?; unfold funcomp. unfold enc_var. rewrite idSubst_exp; trivial. intros y; cbn. destruct (le_lt_dec (length C) y). rewrite it_up_ren_ge, (Nat.add_comm (| C |)), (Nat.add_comm (| C |)), Nat.sub_add, sapp_ge_in; simplify; trivial. erewrite it_up_ren_lt, nth_error_sapp; trivial. erewrite map_nth_error; auto using nth_nats. + unfold enc_const; intros c; destruct (R' c) eqn: ?; cbn; trivial. intros [m H'] % H1 % find_in; trivial; rewrite H'. eapply find_Some, nth_error_Some_lt in H'. cbn; unfold funcomp; erewrite it_up_ren_lt, nth_error_sapp; trivial. erewrite map_nth_error; auto using nth_nats. + intros ? ?; mapinj; mapinj; cbn; rewrite it_up_lt; auto using nats_lt. - unfold enc_const; intros c; destruct (R' c) eqn: ?; cbn; trivial. intros [m H'] % H2 % find_in; trivial; rewrite H'. eapply find_Some, nth_error_Some_lt in H'. now cbn; erewrite it_up_lt. 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)