proposition: Lemma nominal_induction_size : forall n, forall t, size t <= n -> forall P : n_exp -> Type, (forall x, P (n_var x)) -> (forall x t, (forall y, P (swap x y t)) -> P (n_abs x t)) -> (forall t1 t2, P t1 -> P t2 -> P (n_app t1 t2)) -> P t.
proof: Proof. induction n. intros t SZ; destruct t; intros; simpl in SZ; lia. intros t SZ P VAR ABS APP; destruct t; simpl in *. - auto. - apply ABS. intros y. apply IHn; eauto; rewrite swap_size_eq; try lia. - apply APP. apply IHn; eauto; lia. apply IHn; eauto; lia. Defined.
imports: Lia Metalib.Metatheory Metalib.LibLNgen