proposition: Lemma subst_size : forall n (u : n_exp) (x:atom) (t:n_exp), size t <= n -> subst_rec n t u x = subst_rec (size t) t u x.
proof: Proof. intro n. eapply (lt_wf_ind n). clear n. intros n IH u x t SZ. destruct t; simpl in *; destruct n; try lia. - default_simp. - default_simp. rewrite <- (swap_size_eq x0 x1). rewrite <- (swap_size_eq x0 x1) in SZ. apply IH. lia. lia. - simpl. rewrite (IH n); try lia. rewrite (IH n); try lia. rewrite (IH (size t1 + size t2)); try lia. rewrite (IH (size t1 + size t2)); try lia. auto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen