proposition: Lemma sn_lam x u : SN R_aeq u -> SN R_aeq (Lam x u).
proof: Proof. intro h'. assert (h : SN (supterm! U R_aeq) u). apply SN_supterm_R_mon. class. hyp. clear h'. revert h; induction 1; rename x0 into u. apply SN_intro; intros t r. inversion r; clear r; subst. inv_aeq H1; clear H1; subst. permut_rename i0; clear i1. inversion H3; clear H3; subst. apply Rh_eh in H1. inversion H1; clear H1; subst. rewrite rename_app, rename_var, eqb_refl in i. inv_aeq i; clear i; subst. rewrite rename_notin_fv in i1. 2: hyp. rewrite H2, <- i1. apply (SN_incl (supterm! U R_aeq)). apply incl_union_r. refl. apply H. left. apply t_step. apply st_app_l. assert (e : t ~~ Lam x (rename x0 x u')). trans (Lam x0 u'). hyp. apply aeq_alpha'. destruct i2. auto. right. intro h. apply fv_clos_mon in H6; class. rewrite e. apply H0. right. rewrite i. apply subs_R_aeq. refl. apply clos_aeq_intro_refl. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)