proposition: Lemma subs1_seq : forall u s1 s2, (forall x, In x (fv u) -> s1 x = s2 x) -> subs1 s1 u = subs1 s2 u.
proof: Proof. induction u; simpl; intros s1 s2 h. apply h. set_iff. refl. refl. rewrite IHu1 with (s1:=s1) (s2:=s2), IHu2 with (s1:=s1) (s2:=s2); intuition; apply h; set_iff; auto. rewrite IHu with (s1:=update x (Var x) s1) (s2:=update x (Var x) s2). refl. intros y hy. unfold Def.update. eq_dec y x. refl. apply h. set_iff. auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)