proposition: Lemma subs1_single_subs1 y v : forall u s, s y = Var y -> ~In y (fvcodom (fv u) s) -> subs1 (single y v) (subs1 s u) = subs1 (update y v s) u.
proof: Proof. induction u; intros s h1; simpl. rewrite fvcodom_singleton. unfold bool_of_rel. destruct (eq_term_dec (s x) (Var x)). intros _. rewrite e. simpl. unfold Def.single, Def.update. eq_dec x y; auto. intro h2. rewrite subs1_notin_fv. unfold Def.update. eq_dec x y. subst y. tauto. refl. rewrite empty_subset. intro a. rewrite In_domain. unfold Def.single, Def.update. eq_dec a y. subst a. tauto. tauto. refl. rewrite fvcodom_union. set_iff. intro h2. rewrite IHu1, IHu2; auto. intro h2. f_equal. unfold Def.single. eq_dec x y. subst y. rewrite !subs1_update2_eq, !subs1_update_id; auto. apply subs1_id. rewrite subs1_update_id. 2: unfold Def.update; eq_dec x y; tauto. fold (single y v). rewrite IHu, subs1_update2_neq_com. refl. auto. unfold Def.update. eq_dec y x. subst y. tauto. hyp. rewrite fvcodom_update_id. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)