proposition: Lemma neutral_apps : forall n (us : Tes n) u, neutral u -> neutral (apps u us).
proof: Proof. induction us; simpl. auto. intros u nu. apply IHus. apply neutral_app. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)