proposition: Lemma subs_apps s : forall n (us : Tes n) t, subs s (apps t us) = apps (subs s t) (Vmap (subs s) us).
proof: Proof. induction us; intro t; simpl. refl. rewrite IHus. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)