proposition: Lemma size_apps_l : forall n (ts : Tes n) t, size t <= size (apps t ts).
proof: Proof. induction n; intros ts t. VOtac; simpl. refl. VSntac ts; simpl. rewrite <- IHn. simpl. max. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)