proposition: Lemma size_apps_r_in : forall n (ts : Tes n) t ti, Vin ti ts -> size ti < size (apps t ts).
proof: Proof. induction n; intros ts t ti. VOtac; simpl. fo. VSntac ts; simpl. intros [h|h]. rewrite h. eapply Nat.lt_le_trans. 2: apply size_apps_l. simpl. max. apply IHn. hyp. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)