proposition: Lemma HMul_dec : { f: FunctionSymbol | term (appHead M) = ^f /\ term (appHead N) = ^f /\ list2multiset (appArgs M) {>>} list2multiset (appArgs N)} + { term (appHead M) <> term (appHead N) \/ ~list2multiset (appArgs M) {>>} list2multiset (appArgs N) }.
proof: Proof. intros. destruct (funApp_head M Mfa). destruct (isFunApp_dec N) as [Nfa | Nnfa]. destruct (funApp_head N Nfa). destruct (eq_FunctionSymbol_dec x x0). destruct (@mOrd_dec_aux horpo horpo_eq_compat' (list2multiset (appArgs M)) (list2multiset (appArgs N))); trivial. intros. apply IH. left; apply arg_subterm. destruct (member_multiset_list (appArgs M) H) as [w wM mw]. unfold eqA in mw; unfold TermsEqset.eqA in mw; rewrite mw; trivial. left; exists x; repeat split; trivial. rewrite e1; trivial. right; right. intro MN; apply n. inversion MN; trivial. right; left; try_solve. unfold isFunApp in Nnfa. right; left. term_inv (appHead N). Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)