proposition: Lemma dp_incl : forall R1 R2, @inclusion _ R1 R2 -> @inclusion _ (dp R1) (dp R2).
proof: Proof. intros R1' R2' R1_in_R2 t1 t2 H. inversion H as [t1' t2' p f2 l2 H' Subt Df2]; subst. apply (Dp R2' t2 t2' p f2 l2); trivial. apply R1_in_R2; trivial. inversion Df2 as [g2 l u H1]; subst. apply (Def R2' f2 l u). apply R1_in_R2; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)