proposition: Lemma beta_aeq_apps_fun f n (us : Tes n) t : apps (Fun f) us =>b t -> exists vs, t = apps (Fun f) vs /\ clos_vaeq beta us vs.
proof: Proof. intro r. assert (h : not_lam (Fun f)). discr. destruct (beta_aeq_apps_no_lam h r) as [v [vs [h1 h2]]]; clear h r; subst. exists vs. rewrite clos_vaeq_cons in h2. destruct h2 as [[h1 h2]|[h1 h2]]. inv_beta_aeq h1. simpl_aeq. subst. auto. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)