fact: Definition add (s t: exp X) := lambda lambda (ren (shift >> shift) s) ((ren (shift >> shift) t) (var 1) (var 0)) (var 0).
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)