proposition: Lemma rewrite_aeq_apps_fun : forall f n (us : Tes n) t, apps (Fun f) us =>S t -> (exists vs, t = apps (Fun f) vs /\ us ==>S 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 r. inversion r; subst; clear r. rename v' into t'. inv_aeq H; clear H; subst. destruct (rewrite_apps_fun H1) as [[vs [j1 j2]]|[p [ls [r [s [q [vs [h1 [h2 [h3 h4]]]]]]]]]]; clear H1; subst. left. inv_aeq H0; clear H0; subst. exists us1. intuition. exists us0. intuition. exists vs. intuition. right. rewrite Vcast_refl in i1. inv_aeq H0; clear H0; subst. ex p ls r s q vs (Logic.eq_refl (p+q)). split. hyp. rewrite Vcast_refl. intuition. rewrite i0, i2. refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)