proposition: Lemma Hclosed : forall f g, ~G f -> symb_sup R f g -> ~G g.
proof: Proof. intros f g Hf H Gg; apply Hf. rewrite Gdef' in Gg; rewrite Gdef'. inversion Gg as [g' l t [K1 K2]]; clear Gg; subst g'. destruct H as [v [u [[J1 J2] [J3 J4]]]]. destruct u as [x | f' k]. contradiction. subst f'. constructor 1 with k v; split. assumption. intros [x [y [H1 [H2 [f' [H3 H4]]]]]]; apply K2. exists x; exists y; split; [ | split]. assumption. assumption. exists f'; split. assumption. apply refl_trans_clos_is_trans with f. assumption. right; left. constructor 1 with v. exists (Term f k); split; split. assumption. apply eq_refl. assumption. 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)