proposition: Lemma bvcod_rename y z xs : bvcod xs (single y (Var z)) [=] empty.
proof: Proof. rewrite bvcod_single. simpl. destruct (mem y xs); fset. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)