proposition: Lemma restrict_bvcodom_subs_aeq_prop : forall u v ys P, Proper (saeq (union (fv u) (fv v)) ==> Equal) ys -> Proper (saeq (union (fv u) (fv v)) ==> iff) P -> (forall s, dom_incl (union (fv u) (fv v)) s -> inter (bvcod (union (fv u) (fv v)) s) (ys s) [=] empty -> P s -> subs s u ~~ subs s v) -> forall s, P s -> subs s u ~~ subs s v.
proof: Proof. intros u v ys P hys hP h s hs. destruct (saeq_notin_bvcodom (ys s) 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. rewrite <- h1 at 2. hyp. rewrite <- h1. 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)