proposition: Lemma downcast_constants Gamma s t Delta sigma: Delta ⊩ sigma : Gamma -> sigma • s ≡ sigma • t -> exists Sigma tau, Delta ++ Sigma ⊩ tau : Gamma /\ tau • s ≡ tau • t /\ ord' Sigma <= 1 /\ (forall x c, c ∈ consts (tau x) -> c ∈ Consts [s; t]).
proof: Proof. Proof using n Leq. intros [m H] % ordertypingSubst_complete EQ. eapply ordertypingSubst_monotone with (m := S m) in H; trivial. eapply downcast_constants_ordered in H as (Sigma & tau & ?); [|lia|eauto]. exists Sigma; exists tau; intuition trivial. eapply ordertypingSubst_soundness; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)