proposition: Lemma subs_comp u s1 s2 : subs s2 (subs s1 u) ~~ subs (comp s2 s1) u.
proof: Proof. set (A := fvcodom (fv u) s1). set (B := fvcodom (fv (subs s1 u)) s2). set (C := fvcodom (fv u) (comp s2 s1)). set (D := fvcodom (fvcod (fv u) s1) s2). set (P := union A (union B C)). set (Q := union B D). destruct (aeq_notin_bv P u) as [u' [uu' hu']]. rewrite uu'. destruct (saeq_notin_bvcodom Q s1 (fv u')) as [s1' [e1 [h1 h2]]]. rewrite (subs_saeq e1). assert (a : subs s1' u' = subs1 s1' u'). apply subs1_no_alpha. rewrite <- e1. rewrite <- uu' at 2. fold A. rewrite empty_subset, union_subset_1 with (s:=A) (s':=union B C), <- empty_subset. hyp. assert (b : subs s2 (subs s1' u') = subs1 s2 (subs s1' u')). apply subs1_no_alpha. rewrite <- (subs_saeq e1), <- uu' at 2. fold B. rewrite a. rewrite empty_subset, bv_subs1, <- empty_subset. dnf. rewrite union_empty. split. rewrite empty_subset, union_subset_1 with (s:=B) (s':=union A C), <- empty_subset, <- union_assoc, union_sym with (s:=B), union_assoc. hyp. rewrite empty_subset, union_subset_1 with (s:=B) (s':=D), <- empty_subset. hyp. assert (c : subs (comp s2 s1) u' = subs1 (comp s2 s1) u'). apply subs1_no_alpha. rewrite <- uu' at 2. fold C. rewrite empty_subset, union_subset_1 with (s:=C) (s':=union A B), <- empty_subset, union_sym with (s:=C), union_assoc. hyp. rewrite b, a, c, subs1_comp. 2:{ rewrite <- e1. rewrite <- uu' at 2. fold A. rewrite empty_subset, union_subset_1 with (s:=A) (s':=union B C), <- empty_subset. hyp. } apply subs1_saeq. intros x hx. unfold Def.comp1, Def.comp. rewrite (e1 _ hx). sym. apply aeq_refl_eq. apply subs1_no_alpha. assert (d : bv (s1' x) [<=] bvcod (fv u') s1'). intros y hy. rewrite In_bvcod. ex x. auto. assert (e : fv (s1' x) [<=] fvcod (fv u') s1'). intros y hy. rewrite In_fvcod. ex x. auto. rewrite empty_subset, d, e. rewrite <- e1 at 2. rewrite <- uu' at 2. fold D. rewrite union_subset_1 with (s:=D) (s':=B), union_sym, <- empty_subset. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)