proposition: Lemma abstr2_size_ub : forall (t : Term) (v : nat), size (abstr2 v t) <= 3 * size t.
proof: Proof. intros; induction t; qsimpl. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz