proposition: Lemma horpoArgs_dec : forall M Ns, (forall Marg N, subterm Marg M -> {Marg >>= N} + {~Marg >>= N}) -> (forall N, In N Ns -> {M >> N} + {~M >> N}) -> {M [>>] Ns} + {~M [>>] Ns}.
proof: Proof. induction Ns; intros. left; constructor. destruct IHNs; trivial. intros. destruct (X0 N); auto with datatypes. destruct (X0 a); auto with datatypes. left; constructor 2; trivial. destruct (many_one_dec horpoRC (appArgs M) a) as [[Marg [MMarg MargN]] | noSub]. intros. destruct (X x a); try_solve. apply arg_subterm; trivial. left; constructor 3; trivial. exists Marg; trivial. right; intro MaNs; inversion MaNs; try_solve. destruct H2. apply (noSub x); trivial. right; intro MaNs; inversion MaNs; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)