proposition: Lemma well_formed_rdp_step_inv : forall (R1 R2 : relation term), (forall u v, R1 u v -> well_formed u /\ well_formed v) -> (forall s t, R1 s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall u v, R2 u v -> well_formed u /\ well_formed v) -> (forall s t, R2 s t -> forall x, In x (var_list s) -> In x (var_list t)) -> forall s t, well_formed t -> rdp_step (axiom R1) R2 s t -> well_formed s.
proof: Proof. intros R1 R2 W1 R_reg1 W2 R_reg2 s t Wt H. inversion H as [f l1 l2 t3 H' H'']; clear H; subst. inversion H'' as [s' u sigma H Hs Hfl2]; clear H''; subst. apply well_formed_apply_subst_strong. intros x x_in_s'. apply well_formed_remove_term with u. rewrite Hfl2. inversion H' as [l | k1 k2 H'']; subst. trivial. apply well_formed_rwr with R2 (Term f l1); trivial. apply general_context; assumption. rewrite var_in_term_is_sound. apply R_reg1 with s'. assumption. rewrite <- var_in_term_is_sound; assumption. destruct (W1 _ _ H) as [Ws' _]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)