proposition: Theorem NPEadd_ok e1 e2 : (e1 ++ e2 === e1 + e2)%poly.
proof: Proof. intros l. destruct e1, e2; simpl; try reflexivity; try (case ceqb_spec); try intro H; try rewrite H; simpl; try apply eq_refl; try (ring [phi_0]). apply (morph_add CRmorph). Qed.
imports: ZArith_base