proposition: Lemma update_typing n Delta Gamma sigma (s: exp X) x A: Delta ⊩(n) sigma : Gamma -> Delta ⊢(n) s : A -> nth Gamma x = Some A -> Delta ⊩(n) update x s sigma : Gamma.
proof: Proof. intros ??????; unfold update; destruct eq_dec; subst; eauto; congruence. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)