proposition: Lemma TT : (forall f, mark (mark f) = f) -> forall t, t = mark_term (mark_term t).
proof: Proof. intros mark_inv t; case t; [intros v; simpl | intros f l; simpl; rewrite mark_inv]; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)