proposition: Lemma HSub_dec : { Psub } + { ~Psub }.
proof: Proof. intros; unfold Psub. destruct (many_one_dec horpoRC (appArgs M) N) as [[Marg [MMarg MargN]] | noSub]. intros. apply IH_horpoRC; left; apply arg_subterm; trivial. left; exists Marg; trivial. right; intro sub; destruct sub. absurd (x >>= N); trivial. apply noSub; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)