proposition: Lemma subs1_comp : forall u s1 s2, inter (bv u) (fvcodom (fv u) s1) [=] empty -> subs1 s2 (subs1 s1 u) = subs1 (comp1 s2 s1) u.
proof: Proof. induction u; intros s1 s2 h; simpl. refl. refl. rewrite IHu1, IHu2; try refl; revert h; simpl. rewrite union_inter_1, union_empty, fvcodom_union. intros [h1 h2]. rewrite inter_sym, union_inter_1, union_empty in h1, h2. rewrite inter_sym. tauto. rewrite union_inter_1, union_empty, fvcodom_union. intros [h1 h2]. rewrite inter_sym, union_inter_1, union_empty in h1, h2. rewrite inter_sym. tauto. f_equal. rewrite IHu. apply subs1_seq. intros y hy. unfold Def.comp1 at 1. unfold Def.update at -1. eq_dec y x; simpl. apply update_eq. unfold Def.comp1. apply subs1_seq. intros z hz. unfold Def.update. eq_dec z x. 2: refl. subst z. sym. rewrite inter_empty in h. simpl in h. absurd (In x (fvcodom (remove x (fv u)) s1)). apply h. set_iff. auto. rewrite In_fvcodom. exists y. set_iff. intuition. revert hz. rewrite H. simpl. set_iff. hyp. revert h. do 2 rewrite inter_empty. simpl. intros h y hy. rewrite In_fvcodom. intros [z [i1 [i2 i3]]]. revert i2 i3. unfold Def.update. eq_dec z x. subst z. tauto. intros i2 i3. eapply h. set_iff. right. apply hy. rewrite In_fvcodom. exists z. set_iff. intuition. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)