proposition: Lemma R_aeq_apps_fun f n (us : Tes n) t : apps (Fun f) us =>R t -> exists vs, t = apps (Fun f) vs /\ clos_vaeq R us vs.
proof: Proof. intro r. apply R_aeq_alt in r. destruct r as [r|r]. destruct (beta_aeq_apps_fun r) as [vs [h1 h2]]. ex vs. split_all. unfold Rh. eapply clos_vaeq_same. rewrite clos_mon_union. refl. eapply clos_vaeq_incl. apply incl_union_l. refl. hyp. destruct (eta_aeq_apps_fun r) as [vs [h1 h2]]. ex vs. split_all. unfold Rh. eapply clos_vaeq_same. rewrite clos_mon_union. refl. eapply clos_vaeq_incl. apply incl_union_r. refl. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)