proposition: Lemma one_step_one_step : forall R s t, one_step (one_step R) s t <-> one_step R s t.
proof: Proof. intros R s t; split; intro H. revert s H; pattern t; apply term_rec3; clear t. intros v s H; inversion H as [t1 t2 K | ]; clear H; subst. inversion K as [t1 t2 sigma H1 H2 H3]; clear K; subst. inversion H1 as [s1 s2 K | f l1 l2 K]; clear H1; subst. inversion K as [s1 s2 tau K1 K2 K3]; clear K; subst. do 2 rewrite <- subst_comp_is_subst_comp; apply at_top; apply instance; assumption. discriminate. intros f l IHl s H; inversion H as [t1 t2 K | g l1 l2 K1 K2 K3]; clear H; subst. inversion K as [t1 t2 sigma H1 H2 H3]; clear K; subst. inversion H1 as [s1 s2 K | g l1 l2 K]; clear H1; subst. inversion K as [s1 s2 tau K1 K2 K3]; clear K; subst. do 2 rewrite <- subst_comp_is_subst_comp; apply at_top; apply instance; assumption. simpl; right. injection H3; clear H3; intros; subst. revert sigma IHl; induction K as [t1 t2 l K | t l1 l2 K]; intros sigma IHl. left; apply IHl; [left; apply eq_refl | left; apply instance; assumption]. right; apply (IHK sigma (tail_prop _ IHl)). right; revert IHl; induction K1 as [t1 t2 l K | t l1 l2 K]; intros IHl. left; apply IHl; [left; apply eq_refl | assumption]. right; apply (IHK (tail_prop _ IHl)). left; generalize (instance _ s t nil H); do 2 rewrite empty_subst_is_id; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)