proposition: Lemma action_comp f g : forall u, action f (action g u) = action (fun x => f (g x)) u.
proof: Proof. induction u; simpl. refl. refl. rewrite IHu1, IHu2. refl. rewrite IHu. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)