proposition: Lemma downcast_constants_ordered m Gamma s t Delta sigma: 1 <= m -> Delta ⊩(m) sigma : Gamma -> sigma • s ≡ sigma • t -> exists Sigma tau, Delta ++ Sigma ⊩(m) tau : Gamma /\ tau • s ≡ tau • t /\ ord' Sigma <= 1 /\ (forall x c, c ∈ consts (tau x) -> c ∈ Consts [s; t]).
proof: Proof. intros L' T EQ. pose (C0 := Consts [s; t]). pose (C := Consts (map sigma (nats (length Gamma)))). pose (zeta c := match find c C0 with | Some n => const c | None => match find c C with | Some x => inhab X (length Delta + x) (ctype X c) | None => var 0 end end). exists (target' (map (ctype X) C)). exists (sigma >> subst_consts zeta). intuition trivial. - intros ???. eapply ordertyping_preservation_consts. now eapply weakening_ordertyping_app, T. intros c H1. unfold zeta. destruct (find c C0); trivial. + econstructor; eapply typing_constants; eauto. + eapply Consts_consts with (S := (map sigma (nats (length Gamma)))) in H1 as H2. unfold C; eapply find_in in H2 as [y H2]. rewrite H2. eapply ordertyping_monotone, inhab_app, inhab_typing'; trivial. erewrite map_nth_error; trivial. now eapply find_Some. eapply in_map, lt_nats, nth_error_Some_lt; eauto. - rewrite !subst_const_comm_id. now rewrite EQ. all: eapply subst_consts_ident; intros x; rewrite Consts_consts with (S := [s; t]); intuition (auto with datatypes). all: now unfold zeta, C0; eapply find_in in H as [? ->]. - eapply consts_in_subst_consts in H as [d []]. unfold zeta in *. destruct find eqn: H1. + cbn in H0; intuition; subst. eapply find_Some, nth_error_In in H1; exact H1. + destruct (find d C) eqn: H2. all: rewrite ?consts_inhab in H0; cbn in H0; intuition trivial. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)