proposition: Lemma subs1_single_update x x' y' : forall u s, ~In x' (fv u) -> ~In x' (fvcodom (remove x (fv u)) s) -> ~In x' (bv u) -> ~In x (bv u) -> subs1 (single x' (Var y')) (subs1 (update x (Var x') s) u) = subs1 (update x' (Var y') (update x (Var y') s)) u.
proof: Proof. induction u; intro s; simpl; set_iff; intros h1 h2 h3 h4. rename x0 into z. unfold Def.update. eq_dec z x; eq_dec z x'; simpl. unfold Def.single. rewrite update_eq. refl. unfold Def.single. rewrite update_eq. refl. tauto. rewrite subs1_notin_fv. refl. rewrite domain_single, beq_term_var. case_eq (mem x' (fv (s z)) && negb (eqb y' x')). 2: refl. rewrite andb_true_iff, negb_true_iff, eqb_false_iff, <- mem_iff. intros [i1 i2]. absurd (In x' (fvcodom (remove x (singleton z)) s)). hyp. rewrite In_fvcodom. exists z. set_iff. split_all. revert i1. rewrite H. simpl. set_iff. hyp. refl. revert h2. rewrite remove_union, fvcodom_union. set_iff. intro h2. rewrite IHu1, IHu2; auto. rename x0 into z. f_equal. eq_dec z x'. tauto. rewrite subs1_update2_neq_com with (y:=x'). 2: tauto. rewrite subs1_update_id_single. 2: tauto. eq_dec z x. tauto. rewrite subs1_update2_neq_com. 2: tauto. rewrite IHu; auto. 2:{ rewrite In_fvcodom. intros [a [i1 [i2 i3]]]. revert i1 i2 i3. unfold Def.update. eq_dec a z; simpl; set_iff. tauto. intros [i0 i1] i2 i3. apply h2. rewrite In_fvcodom. exists a. set_iff. intuition. } apply subs1_seq. intros a ha. unfold Def.update. eq_dec a x'; eq_dec a x; eq_dec a z; try subst a; try subst x; try subst z; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)