proposition: Lemma action_eq f g : forall u, (forall x, In x (fv u) \/ In x (bv u) -> f x = g x) -> action f u = action g u.
proof: Proof. induction u; intro h; simpl; f_equal. apply h. left. simpl. set_iff. refl. apply IHu1. intros x hx. apply h. simpl. set_iff. destruct hx; tauto. apply IHu2. intros x hx. apply h. simpl. set_iff. destruct hx; tauto. apply h. simpl. set_iff. tauto. apply IHu. intros y hy. apply h. simpl. set_iff. destruct hy; tauto. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)