proposition: Lemma th_sym : forall R t1 t2, th_eq R t1 t2 -> th_eq R t2 t1.
proof: Proof. intro R. intros t1 t2 H; refine (rwr_inv term (sym_refl R) (fun u1 u2 => th_eq R u2 u1) (fun t => t) _ _ _ _ _); trivial. unfold th_eq; intros; apply trans_clos_is_trans with a2; trivial. unfold th_eq; clear t1 t2 H; intros t1 t2 H; apply t_step. assert (axiom_sym : forall t1 t2, axiom (sym_refl R) t1 t2 -> axiom (sym_refl R) t2 t1). clear t1 t2 H; intros t1 t2 H; inversion_clear H as [u1 u2 sigma H']. destruct H' as [H' | [H' | H']]. apply instance; right; left; trivial. apply instance; left; trivial. apply instance; right; right; subst; trivial. generalize t2 H; clear t2 H; pattern t1; apply term_rec3; clear t1. intros v1 t2 H; inversion_clear H as [ H1 H2 H' | f l1 l2 H' ]. apply at_top; apply axiom_sym; trivial. intros f l1 IH t2 H; inversion_clear H as [H1 H2 H' | H1 H2 l2 H']. apply at_top; apply axiom_sym; trivial. apply in_context; generalize l2 H'; clear f t2 l2 H'; induction l1 as [ | t1 l1]. intros l2 H'; inversion H'. intros [ | t2 l2] H'; inversion_clear H' as [ H1 H2 H'' | f l1' l2' H'' ]. apply head_step; apply IH; trivial; left; trivial. apply tail_step; apply IHl1; trivial; intros; apply IH; trivial; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)