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