proposition: Lemma Gdef : forall f, G f -> defined R f.
proof: Proof. intros f Gf; rewrite Gdef' in Gf; inversion Gf as [f' l t [H _]]; subst f'. constructor 1 with l t; assumption. 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)