proposition: Lemma subst_app : forall u x t1 t2, subst u x (n_app t1 t2) = n_app (subst u x t1) (subst u x t2).
proof: Proof. intros. unfold subst. simpl. rewrite (subst_size (size t1 + size t2)). rewrite (subst_size (size t1 + size t2)). auto. lia. lia. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen