proposition: Lemma x_to_x2_commutes_mark : forall sigma f l, apply_subst sigma (mark_term (Term f l)) = (mark_term (apply_subst sigma (Term f l))).
proof: Proof. intros sigma f l; simpl; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)