+ | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
+ napply (ex_intro ????)
+ [ napply (op ? x0 y0)
+ | napply (conj ????)
+ [ napply (op_closed ??????); nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop ?? f ??)]##]
+nqed.
\ No newline at end of file