proposition: Lemma eq_apps_head : forall p (ts : Tes p) q (us : Tes q) a b, apps a ts = apps b us -> nb_args a = nb_args b -> a = b.
proof: Proof. induction ts; destruct us; intros a b e1 e2; simpl in *. hyp. 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 (IHts _ us (App a h) (App b h0) e1 i); intro j. inversion j. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)