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