proposition: Lemma HAppFlat_dec : {Ns : list Term | isPartialFlattening Ns N & M [>>] Ns} + {~exists2 Ns: list Term, isPartialFlattening Ns N & M [>>] Ns }.
proof: Proof. intros. destruct (isApp_dec N). destruct (allPartialFlattenings N) as [Npf Npf_ok]; trivial. destruct (many_one_dec (fun N M => M[>>]N) Npf M) as [[Np [NpNpf MNp]] | No_pf]; trivial. intros. apply horpoArgs_dec. intros; apply IH_horpoRC; left; trivial. intros; apply IH; right; split; trivial. apply (partialFlattening_subterm N x); trivial. apply (proj2 (Npf_ok x)); trivial. left; exists Np; trivial. apply (proj2 (Npf_ok Np)); trivial. right; intro flat; destruct flat. absurd (M [>>] x); trivial. apply No_pf; trivial. apply (proj1 (Npf_ok x)); trivial. right; intro Ns. destruct Ns. apply n. apply partialFlattening_app with x; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)