SWI-Prolog -- subsumes

Documentation
- Reference manual
  - Built-in Predicates
    - Comparison and Unification of Terms
      - Special unification and comparison predicates
        
        unify_with_occurs_check/2
        
        =@=/2
        
        \=@=/2
        
        subsumes_term/2
        
        term_subsumer/3
        
        unifiable/3
        
        ?=/2
- Packages

Availability:built-in

[ISO]subsumes_term(@Generic, @Specific)

True if Generic can be made equivalent to Specific by only binding variables in Generic. The current implementation performs the unification and ensures that the variable set of Specific is not changed by the unification. On success, the bindings are undone.^{70This
predicate is often named subsumes_chk/2
in older Prolog dialects. The current name was established in the ISO
WG17 meeting in Edinburgh (2010). The chk postfix was
considered to refer to determinism as in e.g., memberchk/2.} This predicate respects constraints.

See section 5.6 for defining clauses whose head is unified using single sided unification.