proposition: Lemma neutral_app : forall u v, neutral u -> neutral (App u v).
proof: Proof. intros u v hu. simpl. clear v. revert u hu. induction u; simpl; auto. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)