proposition: Lemma interp_dom_subterm : forall s t p, Interp_dom s -> subterm_at_pos s p = Some t -> Interp_dom t.
proof: Proof. intros s t p Is Sub q g l Sub' Dg. apply Is with (p ++ q); trivial. apply subterm_in_subterm with t; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)