proposition: Lemma sn_beta_apps_fun f n (us : Tes n) : Vforall (SN beta_aeq) us -> SN beta_aeq (apps (Fun f) us).
proof: Proof. intro h. cut (SN (clos_vaeq beta) us). 2: apply sn_clos_vaeq_intro; hyp. clear h. revert us. induction 1. apply SN_intro. intros v r. assert (k : not_lam (Fun f)). discr. destruct (beta_aeq_apps_no_lam k r) as [u [y [h1 h2]]]; subst. rewrite clos_vaeq_cons in h2. destruct h2 as [[i1 i2]|[i1 i2]]. inversion i1; subst. simpl_aeq; subst. inversion H3; subst. inversion H1. simpl_aeq; subst. apply H0. hyp. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)