proposition: Lemma transl_size_lb : forall (n : nat), size (transl (cex_term n)) >= 2^n.
proof: Proof. assert (forall (n m : nat), size (transl (long_term n m)) >= 2^n). induction n; ssimpl. - scrush using (@Coq.Arith.PeanoNat.Nat.nlt_ge, @Coq.Arith.Gt.gt_le_S, @Coq.Arith.Compare_dec.not_ge, @size_nonneg). - assert (size (abstr (m - S n) (transl (long_term n m))) >= 2 * size (transl (long_term n m))). { hauto using (@abstr_size_lb, @no_lams_transl). } assert (size (abstr (m - S n) (transl (long_term n m))) >= 2 * 2 ^ n). { pose proof (IHn m); eauto with zarith. } scrush. - now unfold cex_term. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz