proposition: Lemma comp_saeq : forall xs s1 t1, saeq xs s1 t1 -> forall s2 t2, saeq (fvcod xs s1) s2 t2 -> saeq xs (comp s2 s1) (comp t2 t1).
proof: Proof. intros xs s1 t1 e1 s2 t2 e2 x hx. unfold Def.comp. rewrite (e1 _ hx). apply subs_saeq. intros y hy. apply e2. rewrite In_fvcod. ex x. rewrite (e1 _ hx). auto. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)