diff --git a/src/Refinements/FApp.class.st b/src/Refinements/FApp.class.st
index 75dff07ff..2c57d6ae5 100644
--- a/src/Refinements/FApp.class.st
+++ b/src/Refinements/FApp.class.st
@@ -72,6 +72,26 @@ FApp >> hash [
 	^s hash
 ]
 
+{ #category : #hotel }
+FApp >> monomorphicDeclIn: γ [
+	"Like fappSmtSort but don't go all the way to Z3.
+	 Do we want to keep this layer?"
+	(s isKindOf: FTC) ifFalse: [ self error ].
+	s isSetCon ifTrue: [ self error ].
+	s isMapCon ifTrue: [ self shouldBeImplemented ].
+	s isBitVec ifTrue: [ self shouldBeImplemented ].
+
+	^(s maybeDataIn: γ)
+		ifNil: [ self error]
+		ifNotNil: [ :d |
+			| instance ct_ts ct ts |
+			ct_ts := self unFApp.  ct := ct_ts first.  ts := ct_ts allButFirst.
+			instance := d apply: (ts collect: [ :each | each z3sort: γ ]).
+			instance monomorphicDeclIn: γ
+			
+		]
+]
+
 { #category : #printing }
 FApp >> printOn: aStream [
 	aStream nextPutAll: '(FApp '.
diff --git a/src/Refinements/FTC.class.st b/src/Refinements/FTC.class.st
index 8d40c2559..2c4bc09e5 100644
--- a/src/Refinements/FTC.class.st
+++ b/src/Refinements/FTC.class.st
@@ -52,8 +52,10 @@ FTC >> fappSmtSort: ts originalFApp: anFApp in: γ [
 	^(self maybeDataIn: γ)
 		ifNil: [ (FObj symbol: typeConstructor symbol) fappSmtSort: ts originalFApp: anFApp in: γ ]
 		ifNotNil: [ :d |
+			| instance |
 			d ddVars = ts size ifFalse: [ self error ].
-			d instantiateZ3Sort: (ts collect: [ :t | t z3sort: γ ])
+			instance := d apply: (ts collect: [ :t | t z3sort: γ ]).
+			instance z3sort: γ
 		]
 ]
 
diff --git a/src/Refinements/TC.class.st b/src/Refinements/TC.class.st
index 5fe9e8a9b..78eebd744 100644
--- a/src/Refinements/TC.class.st
+++ b/src/Refinements/TC.class.st
@@ -17,7 +17,19 @@ instance Eq FTycon where
 	^symbol = rhs symbol
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #hotel }
+TC >> apply: ts [
+	| monoSymbol |
+	ts isEmpty ifTrue: [ ^self ].
+	monoSymbol :=
+		'(',
+		symbol,
+		(ts inject: '' into: [ :soFar :thisArgType | ' ', thisArgType printString ]),
+		')'.
+	^TC symbol: monoSymbol
+]
+
+{ #category : #hotel }
 TC >> fTyconSort [
 	^FTC new: self
 ]
@@ -27,7 +39,7 @@ TC >> hash [
 	^symbol hash
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #hotel }
 TC >> isListTC [
 	^symbol isListConName
 ]
diff --git a/src/Refinements/Z3Sort.extension.st b/src/Refinements/Z3Sort.extension.st
index 87df290a1..e9ef207cb 100644
--- a/src/Refinements/Z3Sort.extension.st
+++ b/src/Refinements/Z3Sort.extension.st
@@ -94,6 +94,11 @@ Cf. Types/Sorts.hs
 
 ]
 
+{ #category : #'*Refinements' }
+Z3Sort >> monomorphicDeclIn: _ [ 
+	^self
+]
+
 { #category : #'*Refinements' }
 Z3Sort >> monomorphicSortName [
 	^self printString