proposition: Lemma rpo_closure : forall bb s t u, (rpo bb t s -> rpo bb u t -> rpo bb u s) /\ (rpo bb s t -> rpo bb t s -> False) /\ (rpo bb s s -> False) /\ (rpo_eq bb s t -> rpo_eq bb t s -> equiv s t).
proof: Proof. intros bb s t u; repeat split. intros; apply (@rpo_trans bb u t s); trivial. intros; apply (@rpo_antirefl bb s); apply rpo_trans with t; trivial. apply rpo_antirefl. intros s_le_t t_le_s; destruct s_le_t as [s t s_eq_t | s t s_lt_t]; trivial. destruct t_le_s as [t s t_eq_s | t s t_lt_s]. symmetry; trivial. assert False; [idtac | contradiction]. apply (@rpo_antirefl bb s); apply rpo_trans with t; trivial. 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)