proposition: Lemma rewrite_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. intro f. induction n; intros us t ht. right. VOtac. simpl in ht. inversion ht; subst; clear ht. inversion H; subst; clear H. destruct (rule_ok H1) as [g [n [ls e]]]; subst. rewrite subs_apps in H0. simpl in H0. destruct ls; simpl in *. 2: rewrite apps_app in H0; discr. inversion H0. subst g. clear H0. ex 0 (@Vnil Te) y s 0 (@Vnil Te). assert (a : 0+0=0). refl. ex a. simpl. rewrite Vcast_refl. intuition. inversion ht; subst; clear ht. right. inversion H; subst. destruct (rule_ok H1) as [g [m [ls e]]]; subst. rewrite subs_apps in H0. simpl in H0. gen (eq_apps_fun_head H0); intro e; subst g. gen (eq_apps_fun_nb_args H0); intro e; subst m. gen (eq_apps_nb_args_args H0); intro e. ex (succ n) ls y s 0 (@Vnil Te). assert (a : succ n + 0 = succ n). lia. exists a. simpl. intuition. sym. rewrite Vapp_nil, Vcast_cast, e, Vcast_refl. refl. rewrite (VSn_eq us) in H. simpl in H. rewrite apps_app in H. rewrite <- VSn_eq in H. inversion H; subst; clear H. gen (IHn _ _ H0); intros [[vs [h1 h2]]|[p [ls [r [s [q [vs [h1 [h2 [h3 h4]]]]]]]]]]; subst. left. rewrite app_apps, Vlast_tail. exists (Vadd vs (Vlast (Vhead us) us)). intuition. rewrite (VSn_add us) at 1. apply Vrel1_add_intro. right. intuition. right. rewrite Vcast_refl in h3. ex p ls r s (Datatypes.S q) (Vadd vs (Vlast (Vhead us) us)). assert (h : p + succ q = succ (p+q)). lia. exists h. split. hyp. split. rewrite (VSn_add us) at 1. rewrite h3, Vadd_app. apply Vcast_pi. rewrite Vlast_tail. apply app_apps. left. rewrite (VSn_eq us) in H. simpl in H. rewrite apps_app in H. rewrite <- VSn_eq in H. inversion H; subst; clear H. rewrite Vlast_tail in H0. exists (Vadd (Vremove_last us) v'). split. apply app_apps. rewrite (VSn_add us). apply Vrel1_add_intro. left. rewrite Vremove_last_add. intuition. destruct us; simpl in H. discr. rewrite apps_app in H. discr. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)