proposition: Lemma downcast_variables Gamma s t Delta sigma: Delta ⊩ sigma : Gamma -> sigma • s ≡ sigma • t -> exists Sigma tau, Sigma ⊩ tau : Gamma /\ tau • s ≡ tau • t /\ ord' Sigma <= 1.
proof: Proof. intros. pose (tau x := match nth Delta x with | Some A => inhab X x A | None => var x end). exists (target' Delta). exists (sigma >> subst_exp tau). split; [|split]. - intros ???; eapply preservation_under_substitution; [eauto|]. unfold tau; intros ?? EQ; rewrite EQ. eauto using ordertyping_soundness. - erewrite <-compSubstSubst_exp; trivial. symmetry. erewrite <-compSubstSubst_exp; trivial. symmetry. now rewrite H0. - eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)