proposition: Lemma notin_fv_replace_all x y : x <> y -> forall u, ~In x (fv (replace_all x y u)).
proof: Proof. intro n. induction u; simpl; set_iff; unfold Def.replace_var; try (eq_dec x0 x); fo. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)