diff --git a/src/canary/metta_corelib.pl b/src/canary/metta_corelib.pl
index 8b2ffa0f8db..ce3c7f0aabf 100755
--- a/src/canary/metta_corelib.pl
+++ b/src/canary/metta_corelib.pl
@@ -144,6 +144,9 @@
 % metta_atom_corelib_types( [:, charsToString [-> 'Expression' 'Atom']]).
 % metta_atom_corelib_types( [:, format-args [-> 'Atom' 'Expression' 'Atom']]).
 
+metta_atom_corelib_types( [:, 'unique', [->, 'Atom', 'Atom']]).
+metta_atom_corelib_types( [:, 'subtraction', [->, 'Atom', 'Atom', 'Atom']]).
+
 metta_atom_corelib_types( [:, 'get-metatype', [->, 'Atom', 'Atom']]).
 metta_atom_corelib_types( [:, 'get-type0', [->, 'Atom', 'Atom']]).
 metta_atom_corelib_types( [:, 'get-ftype', [->, 'Atom', 'Atom']]).
diff --git a/src/canary/metta_eval.pl b/src/canary/metta_eval.pl
index 050c12c497b..d9dc8d06573 100755
--- a/src/canary/metta_eval.pl
+++ b/src/canary/metta_eval.pl
@@ -1650,6 +1650,29 @@
    no_repeats_var(YY),
    eval_20(Eq,RetType,Depth,Self,Eval,RetVal),YY=Vars.
 
+
+eval_20(Eq,RetType,Depth,Self,['subtraction',Eval1,Eval2],RetVal):- !,
+    lazy_subtraction(RetVal1^eval_args(Eq,RetType,Depth,Self,Eval1,RetVal1),
+                  RetVal2^eval_args(Eq,RetType,Depth,Self,Eval2,RetVal2),
+                  RetVal).
+
+%% lazy_subtraction(+E1_Call1, +E2_Call2, -E) is nondet.
+%  - Performs a subtraction operation using lazy evaluation.
+%  - It subtracts elements generated by Call2 from those generated by Call1.
+% Arguments:
+%  - E1^Call1: The first goal (Call1) generating elements (E1).
+%  - E2^Call2: The second goal (Call2) generating elements (E2).
+%  - E: The resulting element after subtracting elements of the second set from the first set.
+lazy_subtraction(E1^Call1, E2^Call2, E1) :-
+    % Step 1: Evaluate Call1 to generate E1
+    call(Call1),
+    % Step 2: Use lazy_findall/3 to declare that all elements satisfying Call2 are supposedly in List2
+    lazy_findall(E2, Call2, List2),
+    % Step 3: Perform the subtraction logic
+    % Only return E1 if it is not a member of List2
+    \+ (member(E2, List2), E1 = E2).
+
+
 eval_20(Eq,RetType,Depth,Self,PredDecl,Res):-
   Do_more_defs = do_more_defs(true),
   clause(eval_21(Eq,RetType,Depth,Self,PredDecl,Res),Body),
diff --git a/src/canary/metta_ontology.pfc.pl b/src/canary/metta_ontology.pfc.pl
index a3a66927119..3440e6008cf 100755
--- a/src/canary/metta_ontology.pfc.pl
+++ b/src/canary/metta_ontology.pfc.pl
@@ -459,6 +459,11 @@
 %properties('&corelib','TupleConcat', [data_structures, qhelp("Concatenates tuples."), concatenation]).
 %properties('&corelib','collapseCardinality', [data_structures, qhelp("Collapses structures with cardinality consideration."), manipulation, cardinality]).
 
+% --- Nondet unique,union,intersection,subtraction Operations ---
+properties('&corelib','unique', [nondet_sets, qhelp("Makes nondet results unique."), no_repeats_var]).
+properties('&corelib','subtraction', [nondet_sets, qhelp("It subtracts elements generated by Call2 from those generated by Call1."), lazy_subtraction]).
+
+
 % --- String and Character manipulation ---
 properties('&corelib','stringToChars', [string_operations, qhelp("Convert a string to a list of chars."), string_to_chars]).
 properties('&corelib','charsToString', [string_operations, qhelp("Convert a list of chars to a string."), chars_to_string]).
diff --git a/tests/baseline_compat/hyperon-mettalog_sanity/subtraction_test.metta b/tests/baseline_compat/hyperon-mettalog_sanity/subtraction_test.metta
new file mode 100644
index 00000000000..25c7ccaff95
--- /dev/null
+++ b/tests/baseline_compat/hyperon-mettalog_sanity/subtraction_test.metta
@@ -0,0 +1,70 @@
+;; Test basic subtraction functionality
+;; This checks that subtracting (b c) from (a b c d) correctly returns (a d).
+!(assertEqual
+  (subtract (superpose (a b c d)) (superpose (b c)))
+  (superpose (a d))
+)
+
+;; Test subtraction with multiple subsequent lists
+;; Here, subtracting (b c) and (d) from (a b c d) should result in (a).
+!(assertEqual
+  (subtract (superpose (a b c d)) (superpose (b c)) (superpose (d)))
+  (superpose (a))
+)
+
+;; Test subtraction with nested structures
+;; This test ensures that nested elements like (foo (bar baz)) are handled correctly.
+!(assertEqual
+  (subtract (superpose ((foo bar) (bar baz) qux)) (superpose ((bar baz) qux)))
+  (superpose ((foo bar)))
+)
+
+;; Test subtraction with mixed types
+;; This checks that the function handles lists with symbols, numbers, and mixed content.
+!(assertEqual
+  (subtract (superpose (1 2 3 foo bar)) (superpose (2 foo)))
+  (superpose (1 3 bar))
+)
+
+;; Test subtraction with duplicates
+;; This test ensures that duplicates are treated correctly.
+!(assertEqual
+  (subtract (superpose (a b b c d)) (superpose (b c)))
+  (superpose (a b d))
+)
+
+;; Test subtraction with `unique` applied outside
+;; In this case, `unique` is applied after the subtraction, removing duplicates.
+!(assertEqual
+  (unique (subtract (superpose (a b b c)) (superpose (b c c d))))
+  (superpose (a))
+)
+
+;; Test subtraction with `unique` applied inside
+;; In this test, `unique` is applied to each input set before performing the subtraction.
+!(assertEqual
+  (subtract (unique (superpose (a b b c))) (unique (superpose (b c c d))))
+  (superpose (a))
+)
+
+;; Test variable substitution during subtraction
+;; This ensures that variables can be used and are properly instantiated during the operation.
+!(assertEqual
+  (subtract (superpose ($x $y)) (superpose (b)))
+  (superpose ($x $y))
+)
+
+;; Test subtraction with empty lists
+;; Subtracting an empty list should return the original list.
+!(assertEqual
+  (subtract (superpose (a b c)) (superpose ()))
+  (superpose (a b c))
+)
+
+;; Test subtraction with variables and nested structures
+;; This checks how variables interact with nested lists during subtraction.
+!(assertEqual
+  (subtract (superpose ((foo ?x) (bar $y))) (superpose ((bar $y) (foo qux))))
+  (superpose ((foo ?x)))
+)
+