proposition: Lemma size_apps_r_nth : forall n (ts : Tes n) t i (hi : i<n), size (Vnth ts hi) < size (apps t ts).
proof: Proof. intros n ts t i hi. apply size_apps_r_in. apply Vnth_in. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)