op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
}.
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ≔
op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
}.
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ≔
| #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