proposition: Lemma head_P_in_H : forall mark, (forall u v, P v u -> mrel mark (dp R) v u) -> forall t1 t2 sigma f l, P t1 t2 -> apply_subst sigma t1 = Term f l -> ~G f.
proof: Proof. intros mark P_in_dpR t1 t2 sigma f l K1 K2 K3. rewrite Gdef' in K3; inversion K3 as [f' k t [K4 K5]]; subst f'. apply K5. constructor 1 with t1; exists t2; split. assumption. split. assumption. exists f; split. destruct t1 as [x | f' l']. assert (_D := P_in_dpR _ _ K1); inversion _D as [a b D J1 J2]. inversion D; subst; discriminate. simpl in K2; injection K2; intros; subst f'. simpl; rewrite eq_symb_bool_refl; apply eq_refl. left. 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)