| #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
napply conj; napply op_closed; nassumption ]
nqed.
\ No newline at end of file
| #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
napply conj; napply op_closed; nassumption ]
nqed.
\ No newline at end of file