diff --git a/src/Refinements-Tests/FQPosTest.class.st b/src/Refinements-Tests/FQPosTest.class.st
index 42b968197..dc3a9ed31 100644
--- a/src/Refinements-Tests/FQPosTest.class.st
+++ b/src/Refinements-Tests/FQPosTest.class.st
@@ -493,3 +493,21 @@ wf:
   reft {v: int | $k0}
 '
 ]
+
+{ #category : #tests }
+FQPosTest >> testUndef01 [
+	self provePos: '
+data LL 1 = [
+  | emp { }
+  | con { lHead : @(0), lTail : LL @(0) }
+]
+
+bind 1 undef : {v: func(1, [@(0)]) | Bool true}
+
+constraint:
+  env [1]
+  lhs {v : LL int | v === undef}
+  rhs {v : LL int | 0 toInt < 7}
+  id 1 tag []
+'
+]
diff --git a/src/Refinements/EVar.class.st b/src/Refinements/EVar.class.st
index a2de526af..a562dc3d3 100644
--- a/src/Refinements/EVar.class.st
+++ b/src/Refinements/EVar.class.st
@@ -61,7 +61,7 @@ eCstAtom f@(sym,g) (EVar x) t
 	g := f env.
 	^g∘sym
 		ifFound: [ :s | (s isUndef and: [(sym_ isInt: t) not])
-			ifTrue: [ self shouldBeImplemented ]
+			ifTrue: [ "(`ECst` t) <$> elabAs f t (EApp (eVar tyCastName) (eVar x))" self shouldBeImplemented ]
 			ifFalse: [ super eCstAtom: t inElabEnv: f ] ]
 		alts: [ super eCstAtom: t inElabEnv: f ]
 ]
diff --git a/src/Refinements/PreSort.class.st b/src/Refinements/PreSort.class.st
index f58b4c778..d58566f99 100644
--- a/src/Refinements/PreSort.class.st
+++ b/src/Refinements/PreSort.class.st
@@ -189,11 +189,12 @@ PreSort >> isUndef [
 isUndef :: Sort -> Bool
 Cf. SortCheck.hs
 "
-	| is_srt is srt |
+	| is_srt is srt j |
 	is_srt := self bkAbs.
 	is := is_srt key.  srt := is_srt value.
 	(srt isKindOf: FVar) ifFalse: [ ^false ].
-	^self shouldBeImplemented 
+	j := srt i.
+	^is includes: j
 ]
 
 { #category : #'as yet unclassified' }