proposition: Lemma restrict_bvcodom_subs_aeq : forall ys u v, (forall s, dom_incl (union (fv u) (fv v)) s -> inter (bvcod (union (fv u) (fv v)) s) ys [=] empty -> subs s u ~~ subs s v) -> forall s, subs s u ~~ subs s v.
proof: Proof. intros ys u v h s. destruct (saeq_notin_bvcodom ys s (union (fv u) (fv v))) as [s' [h1 [h2 h3]]]. rewrite subs_saeq with (s':=s'). rewrite subs_saeq with (s:=s) (s':=s'). apply h; hyp. eapply subs_rel_s. refl. unfold flip. eapply union_subset_2. refl. refl. apply h1. eapply subs_rel_s. refl. unfold flip. eapply union_subset_1. refl. refl. apply h1. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)