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; sauto. Reconstr.reasy (@Coq.Arith.PeanoNat.Nat.nlt_ge, @Coq.Arith.Gt.gt_le_S, @Coq.Arith.Compare_dec.not_ge, @size_nonneg) Reconstr.Empty. assert (size (abstr (m - S n) (transl (long_term n m))) >= 2 * size (transl (long_term n m))). Reconstr.reasy (@abstr_size_lb, @no_lams_transl) Reconstr.Empty. 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(Reconstr) PeanoNat Omega