fact: Definition update x v (sigma: fin -> exp X) := fun y => if x == y then v else sigma y.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)