fact: Fixpoint long_term (n m : nat) : Term := match n with | 0 => LLam m (long_app m) | S k => LLam (m - n) (long_term k m) end.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz