proposition: Lemma rpo_antirefl : forall bb s, rpo bb s s -> False.
proof: Proof. intros bb s; pattern s; apply term_rec3_mem; clear s. intros v v_lt_v; inversion v_lt_v. intros f l IHl t_lt_t; inversion t_lt_t as [ f' l' s'' s' s'_mem_l s_le_s' | f' f'' l' l'' f_prec_f H' H1 H2 | f' g' l' l'' Sf Sg f_eq_g L l_lt_l H H1 H2 | f' g' l' l'' Sf Sg f_eq_g l_lt_l ]; clear t_lt_t; subst. apply (IHl s'); trivial. inversion s_le_s' as [u u' s_eq_s' | u u' s_lt_s']; subst. rewrite <- (equiv_rpo_equiv_1 _ s_eq_s'). apply Subterm with s'; trivial; apply Equiv; apply Eq. apply rpo_trans with (Term f l); trivial. apply Subterm with s'; trivial; apply Equiv; apply Eq. apply (prec_antisym Prec) with f; trivial. clear H;induction l as [| t l]. inversion l_lt_l. inversion l_lt_l as [ s t' l' l'' s_lt_t | s t' l' l'' s_eq_t l'_lt_l'' | s l']; subst. apply IHl with t; trivial; left; reflexivity. apply IHl0; trivial. intros s s_in_l; apply IHl; right; trivial. left; apply eq_refl. induction l as [ | s l]. inversion l_lt_l as [a lg ls lc l' l'' ls_lt_alg]; subst. assert (L := permut_length H); discriminate. apply IHl0. intros t t_mem_l; apply IHl; right; trivial. apply rpo_mul_remove_equiv_aux with s s; trivial. apply Eq. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)