proposition: Lemma beta_eta_rewrite_aeq_apps_fun : forall f n (us : Tes n) t, apps (Fun f) us =>R t -> (exists vs, t = apps (Fun f) vs /\ us ==>R vs) \/ (exists p (ls : Tes p) r s q (vs : Tes q) (h : p+q=n), rule (apps (Fun f) ls) r /\ us ~~~ Vcast (Vapp (Vmap (subs s) ls) vs) h /\ t ~~ apps (subs s r) vs).
proof: Proof. intros f n us t h. apply R_aeq_alt in h. destruct h as [[h|h]|h]. left. destruct (beta_aeq_apps_fun h) as [vs [h1 h2]]; subst. ex vs. split_all. eapply incl_elim. rewrite clos_vaeq_alt. apply incl_union_l. apply incl_union_l. refl. hyp. left. destruct (eta_aeq_apps_fun h) as [vs [h1 h2]]; subst. ex vs. split_all. eapply incl_elim. rewrite clos_vaeq_alt. apply incl_union_l. apply incl_union_r. refl. hyp. destruct (rewrite_aeq_apps_fun h) as [[vs [h1 h2]]|[p [ls [r [s [q [vs [h0 [h1 [h2 h3]]]]]]]]]]; clear h. left. ex vs. split_all. eapply incl_elim. rewrite clos_vaeq_alt. apply incl_union_r. refl. hyp. right. ex p ls r s q vs h0. split_all. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)