proposition: Lemma rpo_lt_subterm_dec : forall p v (IH : forall t, Inb term_eq_dec t v = true -> forall p, {lt p t} + {~lt p t}), { a : term | In a v /\ ge a p } + { ~exists a : term, In a v /\ ge a p }.
proof: Proof. intros. destruct (many_one_dec ge v p). intros. destruct (IH x (Inb_intro term_eq_dec x v H) p). left. left. hyp. destruct (term_eq_dec x p). left. right. hyp. right. intro abs. destruct abs; contr. left. exact s. right. intro abs. destruct abs as [a [av ap]]. apply (n a); hyp. Defined.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)