proposition: Lemma well_formed_dp : forall (R1 : relation term), (forall u v, R1 u v -> well_formed u /\ well_formed v) -> forall s t, dp R1 s t -> well_formed s /\ well_formed t.
proof: Proof. intros R1 W1 v u H. inversion H as [u' r p g k r_R_u Sub Dg H2 H3]; clear H; subst; split. destruct (W1 _ _ r_R_u) as [Wr _]. apply well_formed_subterm with r p; assumption. destruct (W1 _ _ r_R_u) as [_ Wu]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)