proposition: Lemma well_formed_one_step : forall (R : relation term), (forall s t, R s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall r l, R r l -> well_formed r /\ well_formed l) -> forall s t, one_step R t s -> well_formed s -> well_formed t.
proof: Proof. intros R R_reg WR t2 t1 H. revert t1 H; pattern t2; apply term_rec3; clear t2. intros v2 t1 H _; inversion H as [t1' t2' H' | f l1 l2 H']; clear H. subst t1' t2'; inversion H' as [r l sigma H'']; clear H'. destruct l as [v | ]; [idtac | discriminate]. apply well_formed_apply_subst_strong. intros x x_in_r; apply well_formed_remove_term with (Var v). rewrite H0; apply eq_refl. rewrite var_in_term_is_sound; apply R_reg with r. assumption. rewrite <- var_in_term_is_sound; assumption. apply (proj1 (WR _ _ H'')). intros f l2 IHl2 t1 H Wfl2. inversion H as [t1' t2' H' | f' l1 l2' H']; clear H. subst t1' t2'; inversion H' as [r l sigma H'']; clear H'. subst t1. apply well_formed_apply_subst_strong. intros x x_in_r; apply well_formed_remove_term with l. rewrite H0; assumption. rewrite var_in_term_is_sound; apply R_reg with r. assumption. rewrite <- var_in_term_is_sound; assumption. apply (proj1 (WR _ _ H'')). subst t1 l2' f'. apply well_formed_fold; split. destruct (well_formed_unfold Wfl2) as [Wl2 _]; clear Wfl2. induction H' as [t1 t2 l H | t l1 l2 H]. intros u [u_eq_t1 | u_in_l]. apply IHl2 with t2. left; reflexivity. subst u; assumption. apply Wl2; left; reflexivity. apply Wl2; right; assumption. intros u [u_eq_t | u_in_l1]. apply Wl2; left; assumption. apply IHH. intros t2 t2_in_l2 t1 H' Wt2; apply IHl2 with t2. right; assumption. assumption. assumption. intros; apply Wl2; right; assumption. assumption. destruct (well_formed_unfold Wfl2) as [_ Af]. rewrite (one_step_list_length_eq H'). assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)