proposition: Lemma remove_constants_ordertyping Gamma s A: Gamma ⊢(n) s : A -> (forall x, x ∈ consts s -> R' x = None -> x ∈ C) -> enc_ctx C Gamma ⊢(n) enc_term C s : enc_type C A.
proof: Proof. Proof using consts_agree O. intros T H. eapply Lambda_ordertyping; simplify; trivial. eapply ordertyping_preservation_consts. eapply ordertyping_weak_preservation_under_substitution; [eassumption|..]. - intros y B H1 H2. unfold enc_var. eapply AppR_ordertyping. + eapply map_var_typing with (L := map (ctype X) C). * intros x; rewrite dom_lt_iff; simplify. intros ? % nats_lt; lia. * rewrite select_nats. rewrite firstn_app; simplify. rewrite <-firstn_all; cbn; now simplify. * auto. + econstructor; simplify; [split;[trivial|]|]. eapply vars_ordertyping_nth with (n := n) (Gamma := Gamma) in H1; eauto. unfold enc_ctx; erewrite nth_error_app2, map_nth_error; simplify; now auto. - intros x H'. unfold enc_const. eapply consts_subst_in in H' as []. destruct (R' x) eqn: EQ. + eapply tight_is_tight in EQ as EQ'; subst x. rewrite <-consts_agree. econstructor. rewrite consts_agree. eapply typing_constants; eauto. + destruct find eqn: H1. * eapply find_Some in H1. econstructor. rewrite <-O. now eapply ord'_in, in_map, H. rewrite nth_error_app1; simplify; eauto using nth_error_Some_lt. erewrite map_nth_error; now auto. * exfalso. eapply find_not_in in H1; intuition. + unfold enc_var in H0. destruct H0. intuition. rewrite consts_AppR in H2. simplify in H2. unfold Consts in H2; eapply in_flat_map in H2 as []. intuition. mapinj. cbn in H3; intuition. 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)