proposition: Lemma well_formed_rwr : 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, rwr R t s -> well_formed s -> well_formed t.
proof: Proof. intros R R_reg WR s t H; induction H as [t1 t2 H | t1 t2 t3 H1 H2]. apply well_formed_one_step with R; trivial. intro Wt3; apply well_formed_one_step with R t2; trivial. apply IHH2; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)