proposition: Lemma eq_apps_args : forall p (ts : Tes p) q (us : Tes q) a b (h1 : apps a ts = apps b us) (h2 : nb_args a = nb_args b), ts = Vcast us (eq_apps_nb_args_sym h1 h2).
proof: Proof. induction ts; destruct us; intros a b e1 e2; simpl in *. rewrite Vcast_refl. refl. gen (f_equal nb_args e1). rewrite apps_app. simpl. rewrite nb_args_apps. lia. gen (f_equal nb_args e1). rewrite apps_app. simpl. rewrite nb_args_apps. lia. assert (i : nb_args (App a h) = nb_args (App b h0)). simpl. lia. gen (eq_apps_head e1 i); intro j. inversion j; subst. match goal with |- _ = Vcast _ ?p => set (h:=p) end. rewrite Vcast_cons. apply Vtail_eq. gen (IHts _ us (App b h0) (App b h0) e1 i); intro k. rewrite k at 1. apply Vcast_pi. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)