proposition: Lemma subs_seq_restrict u s : subs s u = subs (restrict (fv u) s) u.
proof: Proof. apply subs_seq. apply seq_restrict. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)