proposition: Lemma compute_red_unfold : forall t : term, compute_red t = @F_compute_red t (fun y _ => compute_red y).
proof: Proof. intros t; unfold compute_red. refine (Fix_eq _ _ _ _ t). clear t; intros t F G H. unfold F_compute_red; destruct t as [ v | f l ]; simpl; auto. apply (f_equal (fun kk => compute_head_red (Term f l) rule_list ++ (map (fun k => Term f k) kk))). apply mapii_dep_eq. intros t t_in_l; apply H. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)