diff --git a/Refinements-Doodles/ShallowRefinementTest.class.st b/Refinements-Tests/ShallowRefinementTest.class.st
similarity index 86%
rename from Refinements-Doodles/ShallowRefinementTest.class.st
rename to Refinements-Tests/ShallowRefinementTest.class.st
index 1620d0fc1..8c2bce080 100644
--- a/Refinements-Doodles/ShallowRefinementTest.class.st
+++ b/Refinements-Tests/ShallowRefinementTest.class.st
@@ -1,7 +1,7 @@
 Class {
 	#name : #ShallowRefinementTest,
 	#superclass : #TestCaseWithZ3Context,
-	#category : #'Refinements-Doodles'
+	#category : #'Refinements-Tests'
 }
 
 { #category : #'tests - factorial' }
@@ -47,6 +47,14 @@ ShallowRefinementTest >> testInvertFactorial [
 		equals: 5
 ]
 
+{ #category : #'tests - factorial' }
+ShallowRefinementTest >> testNincludes1 [
+	| ℕ |
+	ℕ := Int sort | [ :k | k >= 0 ].
+	self assert: 1 ∈ ℕ.
+	self deny:  -1 ∈ ℕ.
+]
+
 { #category : #'tests - sets' }
 ShallowRefinementTest >> testSubset [
 	| gt1 gt0 |
diff --git a/Refinements/ShallowRefinement.class.st b/Refinements/ShallowRefinement.class.st
index 538129aea..15eaac674 100644
--- a/Refinements/ShallowRefinement.class.st
+++ b/Refinements/ShallowRefinement.class.st
@@ -15,7 +15,7 @@ ShallowRefinement class >> base: B predicate: e [
 		yourself
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> allElements [
 	| nu solver elements |
 	nu := B mkFreshConst: 'nu'.
@@ -33,7 +33,7 @@ ShallowRefinement >> allElements [
 	^elements
 ]
 
-{ #category : #algebra }
+{ #category : #'set theory' }
 ShallowRefinement >> anyOne [
 	| nu solver instance |
 	nu := B mkFreshConst: 'nu'.
@@ -55,6 +55,16 @@ ShallowRefinement >> base: aSort [
 	B := aSort
 ]
 
+{ #category : #'set theory' }
+ShallowRefinement >> includes: x [
+	"Caveat programmator: this is purely a REFINEMENT test,
+	 simply assuming that the sorts agree.
+	 We can't really do much here meaningfully,
+	 because many things can reasonably cast to many other things.
+	 For example, 'a' casts to the integer symbolic constant a."
+	^x∘e
+]
+
 { #category : #accessing }
 ShallowRefinement >> predicate [
 	^e
@@ -81,21 +91,21 @@ ShallowRefinement >> toPredicateOver: varName [
 	^self predicate value: var
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> ∩ [ rhs 
 	B = rhs ifTrue: [ ^self ].
 	B = rhs base ifFalse: [ self error: 'Incoherent sorts' ].
 	^B | [ :x | (e value: x) & (rhs predicate value: x) ]
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> ∪ [ rhs 
 	B = rhs ifTrue: [ ^self ].
 	B = rhs base ifFalse: [ self error: 'Incoherent sorts' ].
 	^B | [ :x | (e value: x) | (rhs predicate value: x) ]
 ]
 
-{ #category : #algebra }
+{ #category : #'set theory' }
 ShallowRefinement >> ⊆ [ rhs
 	| x solver |
 	self base == rhs base ifFalse: [ self error: 'To compare refinement types, first the base types must already be the same' ].