proposition: Lemma HFun_dec: { fg: FunctionSymbol * FunctionSymbol | term (appHead M) = ^(fst fg) /\ term (appHead N) = ^(snd fg) /\ fst fg >#> snd fg /\ M [>>] (appArgs N)} + { ~isFunApp N \/ (forall f g, term (appHead M) = ^f -> term (appHead N) = ^g -> ~f >#> g) \/ ~M [>>] (appArgs N) }.
proof: Proof. intros. destruct (funApp_head M Mfa). destruct (isFunApp_dec N) as [Nfa | Nnfa]. destruct (funApp_head N Nfa). destruct (Prec.Ord_dec x x0). destruct (@horpoArgs_dec M (appArgs N)). intros; apply IH_horpoRC; left; trivial. intros; apply IH; right; split; trivial. apply arg_subterm; trivial. left; exists (x, x0); repeat split; trivial. right; right; right; trivial. right; right; left; intros. rewrite e in H; rewrite e0 in H0. inversion H; inversion H0. rewrite <- H2; rewrite <- H3; trivial. right; left; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)