proposition: Lemma bv_subs1 : forall u s, bv (subs1 s u) [<=] union (bv u) (bvcod (fv u) s).
proof: Proof. induction u; intro s; simpl; set_iff; intro a. intro ha. rewrite union_empty_l, In_bvcod. exists x. set_iff. auto. set_iff. auto. set_iff. rewrite IHu1, IHu2, bvcod_union. set_iff. tauto. set_iff. rewrite IHu. set_iff. rewrite bvcod_update. simpl. destruct (mem x (fv u)); rewrite union_empty_l; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)