proposition: Lemma no_lams_transl2 : forall t : Term, NoLambdas (transl2 t).
proof: Proof. induction t; sauto using no_lams_abstr2. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz