proposition: Lemma saeq_notin_bvcodom : forall ys s xs, exists s', saeq xs s s' /\ inter (bvcod xs s') ys [=] empty /\ dom_incl xs s'.
proof: Proof. intros ys s. apply set_induction_bis. intros xs xs' e [s' [ss' [h1 h2]]]. ex s'. rewrite <- e. auto. ex id. split; try split; intro x; try rewrite bvcod_empty; set_iff; tauto. intros x xs n [s' [ss' [h1 h2]]]. destruct (aeq_notin_bv ys (s x)) as [u [i1 i2]]. ex (update x u s'). split. intro y. set_iff. unfold Def.update. eq_dec y x. subst y. intros. hyp. intros [i|i]. subst y. tauto. apply ss'. hyp. split. rewrite inter_sym, inter_empty. intros y hy. rewrite In_bvcod. intros [z [j1 j2]]. revert j1 j2. set_iff. unfold Def.update. eq_dec z x. subst z. intros _ h'. rewrite inter_empty in i2. eapply i2. apply h'. hyp. intros [h3|h3] h4. subst z. tauto. rewrite inter_sym, inter_empty in h1. absurd (In y (bvcod xs s')). apply h1. hyp. rewrite In_bvcod. ex z. tauto. intro y. set_iff. intro hy. unfold Def.update. eq_dec y x. subst y. tauto. apply h2. tauto. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)