proposition: Lemma unit_nf_nothing : forall f, (unit_theory f = Nothing) -> forall l, unit_nf (Term f l) = Term f (map unit_nf l).
proof: Proof. intros f UT [ | t1 [ | t2 [ | t3 l]]]. trivial. simpl; destruct (unit_nf t1) as [ v1 | f1 [ | s1 l1]]; trivial. simpl; destruct (unit_nf t1) as [ v1 | f1 [ | s1 l1]]; destruct (unit_nf t2) as [ v2 | f2 [ | s2 l2]]; trivial; repeat rewrite UT; trivial. simpl; destruct (unit_nf t1) as [ v1 | f1 [ | s1 l1]]; destruct (unit_nf t2) as [ v2 | f2 [ | s2 l2]]; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)