proposition: Lemma apps_app : forall n (us : Tes n) t u, apps (App t u) us = App (apps t (Vremove_last (Vcons u us))) (Vlast u us).
proof: Proof. induction us; intros t u; simpl. refl. rewrite IHus. apply (f_equal (fun v => App (apps (App t u) v) (Vlast h us))). unfold Vremove_last. rewrite Vsub_cons. apply Vsub_pi. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)