fact: Fixpoint compute_head_red s rule_list {struct rule_list} : list term := match rule_list with | nil => nil | (l,r) :: rule_list => match matching ((l,s) :: nil) with | Some sigma => (apply_subst sigma r) :: compute_head_red s rule_list | None => compute_head_red s rule_list end end.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)