proposition: Lemma rwr_at_top_not_H : forall l r, R r l -> (match l with Var _ => False | Term g _ => G g end) -> forall sigma, Interp_dom (apply_subst sigma l) -> Interp_dom (apply_subst sigma r) -> forall s' t', Interp (apply_subst sigma l) s' -> Interp (apply_subst sigma r) t' -> rwr (Pi pi V0 V1) t' s'.
proof: Proof. intros l r K K' sigma Acc_ls Acc_rs s' t' Il Ir. destruct l as [ | f l]. contradiction. simpl in Il; inversion Il; clear Il; subst. absurd (G f); assumption. apply project_comb; right. rewrite in_map_iff; exists (apply_subst sigma r, t'); split; trivial. assert (rs_in_kk : In (apply_subst sigma r) (map (fun st : term * term => fst st) kk)). rewrite <- H5; rewrite FB; left; apply (instance R r (Term f l) sigma); assumption. rewrite in_map_iff in rs_in_kk. destruct rs_in_kk as [[rs t''] [K1 K2]]; simpl in K1; subst. assert (Acc_rs' : Acc interp_call (apply_subst sigma r)). apply interp_well_defined; trivial. rewrite (interp_unicity (apply_subst sigma r) Acc_rs' t' t''); trivial. apply H8; 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)