proposition: Lemma eta_aeq_apps_fun f n (us : Tes n) t : apps (Fun f) us =>e t -> exists vs, t = apps (Fun f) vs /\ us ==>e vs.
proof: Proof. intro r. destruct (eta_aeq_apps r) as [v [vs [h1 h2]]]; clear r; subst. ex vs. rewrite clos_vaeq_cons in h2. destruct h2 as [[h1 h2]|[h1 h2]]. inv_eta_aeq h1. simpl_aeq. subst. auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil VecOrd VecUtil)