proposition: Lemma interp_dom_R2 : forall R1 R2, module R1 R2 -> (forall f, {defined R2 f}+{~defined R2 f}) -> (forall s t, R1 s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall v t, ~ R2 t (Var v)) -> forall (s t : term), Interp_dom R1 R2 s -> one_step R2 t s -> Interp_dom R1 R2 t.
proof: Proof. intros R1 R2 module_R1_R2 def_dec R1_reg R2_var; intros s t Is H; apply (interp_dom_R1_R2 R1 R2 module_R1_R2 def_dec R1_reg R2_var s); trivial. rewrite split_rel; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)