proposition: Lemma Uempty_initial_strong_axioms : forall a : E, strong_axioms (Uempty_initial a).
proof: Proof. ir. uf Uempty_initial. ap inclusion_strong_axioms. rw underlying_Uempty. uf sub; ir. nin H. elim x0. Qed.
imports: Arith functions