proposition: Lemma irreflexive_lt_mpo : irreflexive ltF -> irreflexive lt_mpo.
proof: Proof. intro ltF_irrefl. intros s; induction s as [x | f ss IHs] using term_ind_forall2; intro H; inversion H; subst. apply (ltF_irrefl f); trivial. gen H1; apply irrefl_to_mult_irrefl. unfold eqA,Term.eqA; intros; subst; trivial. unfold eqA,Term.eqA; intros; subst; trivial. intros x y z; unfold transp; simpl; intros; apply transitive_lt_mpo with y; trivial. unfold transp; simpl; intros s s_in_ss Hs; apply (IHs s); trivial. elim H2; intros s Hs; elim Hs; clear Hs; intros s_in_ss Hs. elim Hs; clear Hs; intro case_s. apply (IHs s); subst; trivial. apply (IHs s s_in_ss). apply transitive_lt_mpo with (Fun f ss); trivial. constructor 3; exists s; split; trivial; left; trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)