Size

Require Import internalize_tac Encoding Nat bijection.

Internalized size of terms

Instance term_size : internalized size.
Proof.
  internalizeR. induction y;recStep P; crush.
Defined.

Lemma size_surj : surjective size.
Proof.
  intros n. induction n.
  - exists 0. reflexivity.
  - destruct IHn as [t H]. exists (lam t). simpl; congruence.
Qed.