proposition: Lemma th_eq_closure_one_step : forall (R : term -> term -> Prop), forall t1 t2, one_step (rwr R) t1 t2 -> rwr R t1 t2.
proof: Proof. intros R t1; pattern t1; apply term_rec3; clear t1. intros x1 t2 H; inversion_clear H as [ t1' t2' H' | ]; inversion_clear H'; apply rwr_apply_subst; trivial. intros f1 l1 Hrec t2 H; inversion_clear H as [ t1' t2' H' | f' l1' l2 H']. inversion_clear H'; apply rwr_apply_subst; trivial. apply general_context; generalize l2 H'; clear l2 H'. induction l1 as [ | a1 l1 ]; intros l2 H. inversion H. inversion H as [ H1 a2 H3 a1_R_a2 H5 H6 | H1 H2 l2' l1_R_l2' H5 H6]; subst. generalize (Hrec _ (or_introl _ (eq_refl _)) _ a1_R_a2). clear; intro H; induction H as [a1 a2 H | a1 a2 a3 H1 H2]. do 2 left; assumption. right with (a2 :: l1); trivial. left; assumption. generalize (IHl1 (tail_prop _ Hrec) l2' l1_R_l2'). clear; intro H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. apply trans_clos_is_trans with (a1 :: l2); trivial. left; right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)