diff --git a/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st b/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st
index b06cda858..30b946d5b 100644
--- a/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st
+++ b/src/SpriteLang-Tests/BoolGaloisConnectionTest.class.st
@@ -93,7 +93,6 @@ BoolGaloisConnectionTest >> testAlphaClash [
 	 so must end up in the same UNSAFE result.
 	 However, this breaks, see issue #139.
 	"
-	self skip. "Remove this skip after #139 is resolved."
 	self proveUnsafe: '
 ⟦val b2i : b:bool => int[i | ((i===0) not <=> b) & ((i===0)|(i===1)) ] ⟧
 let b2i = (b) => {
diff --git a/src/SpriteLang/Alt.class.st b/src/SpriteLang/Alt.class.st
index 90866844b..a67809d1c 100644
--- a/src/SpriteLang/Alt.class.st
+++ b/src/SpriteLang/Alt.class.st
@@ -59,3 +59,11 @@ Alt >> expr [
 Alt >> expr: anObject [
 	expr := anObject
 ]
+
+{ #category : #'α-renaming' }
+Alt >> uniq2: α [
+	^self class
+		daCon: daCon
+		binds: (binds collect: [ :each | each uniq2: α])
+		expr: (expr uniq2: α)
+]
diff --git a/src/SpriteLang/EAnn.class.st b/src/SpriteLang/EAnn.class.st
index 79cfa9f54..24a14458b 100644
--- a/src/SpriteLang/EAnn.class.st
+++ b/src/SpriteLang/EAnn.class.st
@@ -72,3 +72,13 @@ EAnn >> synth: Γ [
 	c := expr check: Γ rtype: t.
 	^{ c . t }
 ]
+
+{ #category : #'α-renaming' }
+EAnn >> uniq2: α [
+
+	^self class
+		expr: (expr uniq2: α)
+		ann:  (ann uniq2: α)
+
+
+]
diff --git a/src/SpriteLang/ECase.class.st b/src/SpriteLang/ECase.class.st
index 8d3856097..153c5a5b1 100644
--- a/src/SpriteLang/ECase.class.st
+++ b/src/SpriteLang/ECase.class.st
@@ -58,6 +58,16 @@ ECase >> goSubsTyExpr: su [
 		])
 ]
 
+{ #category : #'α-renaming' }
+ECase >> uniq2: α [
+	| x′ alts′ |
+	x′ := α at: x ifAbsent:[x].
+	alts′ := alts collect: [ :each | each uniq2: α ].
+	^self class
+		x: x′ alts: alts′
+
+]
+
 { #category : #accessing }
 ECase >> x [
 	^ x
diff --git a/src/SpriteLang/ECon.class.st b/src/SpriteLang/ECon.class.st
index b77b2602e..9f07cb6dd 100644
--- a/src/SpriteLang/ECon.class.st
+++ b/src/SpriteLang/ECon.class.st
@@ -59,3 +59,8 @@ ECon >> synthImm: Γ [
 ECon >> toFX [
 	^self shouldBeImplemented 
 ]
+
+{ #category : #'α-renaming' }
+ECon >> uniq2: α [
+	"Nothing to do"
+]
diff --git a/src/SpriteLang/EFun.class.st b/src/SpriteLang/EFun.class.st
index f56832a8c..7a7621ef8 100644
--- a/src/SpriteLang/EFun.class.st
+++ b/src/SpriteLang/EFun.class.st
@@ -90,3 +90,16 @@ EFun >> renameTy: ty metric: m [
 	t′′_m′ := expr renameTy: t′ metric: m.  t′′ := t′′_m′ key. m′ := t′′_m′ value.
 	^(TFun x: x s: s′ t: t′′) -> m′
 ]
+
+{ #category : #'α-renaming' }
+EFun >> uniq2: α [
+	| id id′ α′ |
+
+	id  := bind id.
+	id′ := id uniq.
+	α′  := α extMap: id to: id′.
+
+	^self class
+		bind: (bind uniq2: α′)
+		expr: (expr uniq2: α′)
+]
diff --git a/src/SpriteLang/EIf.class.st b/src/SpriteLang/EIf.class.st
index 81d1fa4f9..d6684bfed 100644
--- a/src/SpriteLang/EIf.class.st
+++ b/src/SpriteLang/EIf.class.st
@@ -77,3 +77,12 @@ EIf >> trueE [
 EIf >> trueE: anObject [
 	trueE := anObject
 ]
+
+{ #category : #'α-renaming' }
+EIf >> uniq2: α [
+	^self class
+		cond: (cond uniq2: α)
+		trueE: (trueE uniq2: α)
+		falseE: (falseE uniq2: α).
+
+]
diff --git a/src/SpriteLang/EImm.class.st b/src/SpriteLang/EImm.class.st
index 6a52d6ede..e94ab2f5d 100644
--- a/src/SpriteLang/EImm.class.st
+++ b/src/SpriteLang/EImm.class.st
@@ -51,3 +51,14 @@ EImm >> synth: Γ [
 	t := imm synthImm: Γ.
 	^{ HCstr cTrue . t }
 ]
+
+{ #category : #'as yet unclassified' }
+EImm >> uniq [
+	"Nothing to do. This is only called on 'sentinel' EImm terminating list of ELet decls"
+]
+
+{ #category : #'α-renaming' }
+EImm >> uniq2: α [
+	^self class imm: (imm uniq2: α)
+
+]
diff --git a/src/SpriteLang/ELet.class.st b/src/SpriteLang/ELet.class.st
index ae99adf2c..5038af17e 100644
--- a/src/SpriteLang/ELet.class.st
+++ b/src/SpriteLang/ELet.class.st
@@ -79,3 +79,38 @@ ELet >> goSubsTyExpr: su [
 ELet >> gtChildren [
 	^{decl . expr}
 ]
+
+{ #category : #'α-renaming' }
+ELet >> uniq [
+	"α-rename all variables ensuring all have unique names.
+	 Returns a new instance."
+
+	| α decl′ expr′ |
+
+	α := αRenames empty.
+	decl′ := decl class bind: decl bind expr: (decl expr uniq2: α).
+	expr′ := expr uniq.
+
+	^self class
+		decl: decl′
+		expr: expr′
+
+
+
+
+]
+
+{ #category : #'α-renaming' }
+ELet >> uniq2: α [
+	| id id′ α′ decl′ expr′ |
+
+	id := decl bind id.
+	id′:= id uniq.
+	α′ := α extMap: id to: id′.
+
+	decl′ := decl class bind: (decl bind uniq2: α′) expr: (decl expr uniq2: α)."<-- CERTAINLY NOT α!!!"
+	expr′ := expr uniq2: α′.
+
+	^self class decl: decl′ expr: expr′
+
+]
diff --git a/src/SpriteLang/ERApp.class.st b/src/SpriteLang/ERApp.class.st
index 701bc5327..64a6b773b 100644
--- a/src/SpriteLang/ERApp.class.st
+++ b/src/SpriteLang/ERApp.class.st
@@ -41,3 +41,10 @@ ERApp >> synth: Γ [
 	s′ := s rinst.
 	^{ c . s′ }
 ]
+
+{ #category : #'α-renaming' }
+ERApp >> uniq2: α [
+	^self class
+		expr: (expr uniq2: α)
+
+]
diff --git a/src/SpriteLang/ETApp.class.st b/src/SpriteLang/ETApp.class.st
index eb179cba1..2b665d46e 100644
--- a/src/SpriteLang/ETApp.class.st
+++ b/src/SpriteLang/ETApp.class.st
@@ -55,3 +55,11 @@ ETApp >> synth: Γ [
 	tt := Γ refresh: rtype.
 	^{ ce . te type tsubst: tt tVar: te var }
 ]
+
+{ #category : #'α-renaming' }
+ETApp >> uniq2: α [
+	^self class
+		expr: (expr uniq2: α)
+		rtype: (rtype uniq2: α)
+
+]
diff --git a/src/SpriteLang/ETLam.class.st b/src/SpriteLang/ETLam.class.st
index 82b14b59f..fca63bddc 100644
--- a/src/SpriteLang/ETLam.class.st
+++ b/src/SpriteLang/ETLam.class.st
@@ -64,3 +64,8 @@ ETLam >> tvar [
 ETLam >> tvar: anObject [
 	tvar := anObject
 ]
+
+{ #category : #'α-renaming' }
+ETLam >> uniq2: α [
+	self shouldBeImplemented
+]
diff --git a/src/SpriteLang/EVar.extension.st b/src/SpriteLang/EVar.extension.st
index d72f4e983..865f4c3ef 100644
--- a/src/SpriteLang/EVar.extension.st
+++ b/src/SpriteLang/EVar.extension.st
@@ -53,3 +53,12 @@ synthImm :: Env -> SrcImm -> CG RType
 	t := Γ getEnvDamit: sym. 
 	^t singleton: sym
 ]
+
+{ #category : #'*SpriteLang' }
+EVar >> uniq2: α [
+	| sym′ |
+
+	sym′ := α at: sym ifAbsent:[ ^ self ].
+	^self class of: sym′
+
+]
diff --git a/src/SpriteLang/Expr.extension.st b/src/SpriteLang/Expr.extension.st
index 4a6d2de6f..b4fa28b12 100644
--- a/src/SpriteLang/Expr.extension.st
+++ b/src/SpriteLang/Expr.extension.st
@@ -11,6 +11,21 @@ predRType p = TBase TBool (known $ F.predReft p)
 		r: self "F."predReft known
 ]
 
+{ #category : #'*SpriteLang' }
+Expr >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	| self′ |
+
+	self′ := self.
+	α keysAndValuesDo: [ :orig :uniq |
+		self′ := self′ rename: orig to: uniq.
+	].
+	^ self′
+
+
+]
+
 { #category : #'*SpriteLang' }
 Expr >> ΛpredReft [
 	^self predReft known
diff --git a/src/SpriteLang/HPred.extension.st b/src/SpriteLang/HPred.extension.st
index daa68fd8a..b3bceae02 100644
--- a/src/SpriteLang/HPred.extension.st
+++ b/src/SpriteLang/HPred.extension.st
@@ -47,3 +47,11 @@ smash p           = [p]
 HPred >> subsAR: p ar: ar [
 	^self "No κ-apps can happen, because those have been refactored to RefVarApps"
 ]
+
+{ #category : #'*SpriteLang' }
+HPred >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self shouldBeImplemented
+
+]
diff --git a/src/SpriteLang/HPredAnd.extension.st b/src/SpriteLang/HPredAnd.extension.st
index 50c41cae2..ef2ad778a 100644
--- a/src/SpriteLang/HPredAnd.extension.st
+++ b/src/SpriteLang/HPredAnd.extension.st
@@ -23,3 +23,9 @@ HPredAnd >> subs: p ar: ar [
 HPredAnd >> subsAR: aString ar: anARef [
 	^HPredAnd of: (ps collect: [ :each | each subsAR: aString ar: anARef ])
 ]
+
+{ #category : #'*SpriteLang' }
+HPredAnd >> uniq2: α [
+	^self class of: (ps collect: [:e|e uniq2: α])
+
+]
diff --git a/src/SpriteLang/HReft.extension.st b/src/SpriteLang/HReft.extension.st
index a456f5d2a..40da0e06d 100644
--- a/src/SpriteLang/HReft.extension.st
+++ b/src/SpriteLang/HReft.extension.st
@@ -14,3 +14,9 @@ HReft >> predExprsGo [
 HReft >> subs: p ar: ar [
 	^self
 ]
+
+{ #category : #'*SpriteLang' }
+HReft >> uniq2: α [
+	^self class expr: (expr uniq2: α)
+
+]
diff --git a/src/SpriteLang/KnownReft.class.st b/src/SpriteLang/KnownReft.class.st
index 728651464..c30804652 100644
--- a/src/SpriteLang/KnownReft.class.st
+++ b/src/SpriteLang/KnownReft.class.st
@@ -163,3 +163,14 @@ KnownReft >> symbol: anObject [
 KnownReft >> syms [
 	^{symbol}, expr syms
 ]
+
+{ #category : #'α-renaming' }
+KnownReft >> uniq2: α [
+	| symbol′ α′ expr′ |
+
+	symbol′ := symbol uniq.
+	α′ := α extMap: symbol to: symbol′.
+	expr′ := expr uniq2: α′.
+
+	^self class symbol: symbol′ expr: expr′
+]
diff --git a/src/SpriteLang/MetricExpression.class.st b/src/SpriteLang/MetricExpression.class.st
index 05cccd390..38166a7e0 100644
--- a/src/SpriteLang/MetricExpression.class.st
+++ b/src/SpriteLang/MetricExpression.class.st
@@ -59,6 +59,13 @@ MetricExpression >> subst: su [
 	^self class source: replacement sym
 ]
 
+{ #category : #'α-renaming' }
+MetricExpression >> uniq2: α [
+
+	self shouldBeImplemented
+
+]
+
 { #category : #'as yet unclassified' }
 MetricExpression >> wfExpr: γ sort: t [
 "
diff --git a/src/SpriteLang/Prog.class.st b/src/SpriteLang/Prog.class.st
index 2fbb23535..d82f01d77 100644
--- a/src/SpriteLang/Prog.class.st
+++ b/src/SpriteLang/Prog.class.st
@@ -82,11 +82,13 @@ Prog >> solve [
 
 { #category : #verification }
 Prog >> vcgen [
-	| env eL cstr query |
+	| expr′ env expr′′ cstr query |
+
+	expr′ := expr uniq.
 	env := ΓContext empEnv: meas typs: data.
-	eL := expr elaborate: env.
+	expr′′ := expr′ elaborate: env.
 	CGState reset.
-	cstr := eL check: env rtype: TInt instance bTrue.
+	cstr := expr′′ check: env rtype: TInt instance bTrue.
 	query := HornQuery new.
 	cstr addToQuery: query.
 	CGState current cgInfo cgiKVars do: [ :kVar | kVar addToQuery: query ].
diff --git a/src/SpriteLang/RType.class.st b/src/SpriteLang/RType.class.st
index 01119e7d5..fe955cdf8 100644
--- a/src/SpriteLang/RType.class.st
+++ b/src/SpriteLang/RType.class.st
@@ -516,6 +516,13 @@ unify :: F.SrcSpan -> RType -> RType -> ElabM RType
 	^t2 dispatchUnify: self
 ]
 
+{ #category : #'α-renaming' }
+RType >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self subclassResponsibility.
+]
+
 { #category : #'as yet unclassified' }
 RType >> ≺ [ t
 	self subclassResponsibility 
diff --git a/src/SpriteLang/RefVarApp.extension.st b/src/SpriteLang/RefVarApp.extension.st
index b813bcc34..5d8ebe568 100644
--- a/src/SpriteLang/RefVarApp.extension.st
+++ b/src/SpriteLang/RefVarApp.extension.st
@@ -27,3 +27,10 @@ go (H.Var k xs) | k == p ...
 	θ := yts zip: xs with: [ :y_☐ :x | y_☐ key -> x ].
 	^pr substs: θ
 ]
+
+{ #category : #'*SpriteLang' }
+RefVarApp >> uniq2: α [
+
+	self shouldBeImplemented
+
+]
diff --git a/src/SpriteLang/Refl.class.st b/src/SpriteLang/Refl.class.st
index e34c4efa2..b59535314 100644
--- a/src/SpriteLang/Refl.class.st
+++ b/src/SpriteLang/Refl.class.st
@@ -3,3 +3,10 @@ Class {
 	#superclass : #SpriteAnn,
 	#category : #SpriteLang
 }
+
+{ #category : #'α-renaming' }
+Refl >> uniq2: α [
+
+	self shouldBeImplemented
+
+]
diff --git a/src/SpriteLang/SpriteAnn.class.st b/src/SpriteLang/SpriteAnn.class.st
index 25d673470..19a7f5093 100644
--- a/src/SpriteLang/SpriteAnn.class.st
+++ b/src/SpriteLang/SpriteAnn.class.st
@@ -92,3 +92,15 @@ SpriteAnn >> symbol [
 SpriteAnn >> symbol: anObject [
 	symbol := anObject
 ]
+
+{ #category : #'α-renaming' }
+SpriteAnn >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	^self class
+		symbol: symbol
+		rtype: (rtype uniq2: α)
+		metric: (metric ifNotNil:[metric uniq2: α])
+
+
+]
diff --git a/src/SpriteLang/SpriteBind.class.st b/src/SpriteLang/SpriteBind.class.st
index 8f4ec3896..ebafcdeff 100644
--- a/src/SpriteLang/SpriteBind.class.st
+++ b/src/SpriteLang/SpriteBind.class.st
@@ -7,6 +7,11 @@ Class {
 	#category : #SpriteLang
 }
 
+{ #category : #accessing }
+SpriteBind class >> id: id [
+	^self basicNew id: id; yourself
+]
+
 { #category : #accessing }
 SpriteBind class >> identifier: id [
 	^self basicNew id: id; yourself
@@ -29,3 +34,8 @@ SpriteBind >> printOn: aStream [
 		nextPutAll: id;
 		nextPutAll: '"'
 ]
+
+{ #category : #'α-renaming' }
+SpriteBind >> uniq2: α [
+	^self class id: (α at: id ifAbsent:[id])
+]
diff --git a/src/SpriteLang/String.extension.st b/src/SpriteLang/String.extension.st
index 003ea278c..82ca5d0ea 100644
--- a/src/SpriteLang/String.extension.st
+++ b/src/SpriteLang/String.extension.st
@@ -43,3 +43,10 @@ rVar :: F.Symbol -> RType
 String >> unifyX: anotherString [ 
 	^self
 ]
+
+{ #category : #'*SpriteLang' }
+String >> uniq [
+	"Return new unique variable name suitable for
+	 α-renaming."
+	^self, '__ß', VariableAlphabet nextJ printString
+]
diff --git a/src/SpriteLang/TAll.class.st b/src/SpriteLang/TAll.class.st
index 3c0b99bc1..59758fbc8 100644
--- a/src/SpriteLang/TAll.class.st
+++ b/src/SpriteLang/TAll.class.st
@@ -154,6 +154,17 @@ TAll >> type: anObject [
 	type := anObject
 ]
 
+{ #category : #'α-renaming' }
+TAll >> uniq2: α [
+	| α′ var′ type′ |
+
+	var′ := var uniq.
+	α′ := α extMap: var to: var′.
+	type′ := type uniq2: α′.
+
+	^self class var: var′ type: type′
+]
+
 { #category : #accessing }
 TAll >> var [
 	^ var
diff --git a/src/SpriteLang/TBase.class.st b/src/SpriteLang/TBase.class.st
index 4303c8db2..bed1cc8ab 100644
--- a/src/SpriteLang/TBase.class.st
+++ b/src/SpriteLang/TBase.class.st
@@ -214,6 +214,12 @@ TBase >> unifyLL: t [
 	self error: 'Cant unify'
 ]
 
+{ #category : #'α-renaming' }
+TBase >> uniq2: α [
+	^self class b: (b uniq2: α) r: (r uniq2: α)
+
+]
+
 { #category : #'as yet unclassified' }
 TBase >> ≺ [ t
 "
diff --git a/src/SpriteLang/TBool.class.st b/src/SpriteLang/TBool.class.st
index a5c9789e0..a4fa7230c 100644
--- a/src/SpriteLang/TBool.class.st
+++ b/src/SpriteLang/TBool.class.st
@@ -22,3 +22,8 @@ TBool >> baseSort [
 TBool >> printOn: aStream [
 	aStream nextPutAll: 'TBool'
 ]
+
+{ #category : #'α-renaming' }
+TBool >> uniq2: α [
+	"Nothing to do"
+]
diff --git a/src/SpriteLang/TCon.class.st b/src/SpriteLang/TCon.class.st
index ccfc24690..0299a84d9 100644
--- a/src/SpriteLang/TCon.class.st
+++ b/src/SpriteLang/TCon.class.st
@@ -250,6 +250,16 @@ TCon >> unifyLL: tcon2 [
 	^TCon c: c ts: newTs ars: #() r: ΛReft new
 ]
 
+{ #category : #'α-renaming' }
+TCon >> uniq2: α [
+	^self class
+		c: c
+		ts: (ts collect: [ :each | each uniq2: α])
+		ars: (ars collect: [ :each | each uniq2: α])
+		r: (r collect: [ :each | each uniq2: α])
+
+]
+
 { #category : #'as yet unclassified' }
 TCon >> ≺ [ tcon2
 "
diff --git a/src/SpriteLang/TFun.class.st b/src/SpriteLang/TFun.class.st
index f42272436..c972e27e8 100644
--- a/src/SpriteLang/TFun.class.st
+++ b/src/SpriteLang/TFun.class.st
@@ -238,6 +238,19 @@ TFun >> unifyLL: tfun2 [
 	^TFun x: x_ s: s_ t: t_
 ]
 
+{ #category : #'α-renaming' }
+TFun >> uniq2: α [
+	| α′ x′ s′ t′ |
+
+	x′ := x uniq.
+	α′ := α extMap: x to: x′.
+	s′ := s uniq2: α′.
+	t′ := t uniq2: α′.
+
+	^self class x:x′ s:s′ t:t′
+
+]
+
 { #category : #accessing }
 TFun >> x [
 	^ x
diff --git a/src/SpriteLang/TInt.class.st b/src/SpriteLang/TInt.class.st
index eeaa29cc7..2b4dc50c6 100644
--- a/src/SpriteLang/TInt.class.st
+++ b/src/SpriteLang/TInt.class.st
@@ -22,3 +22,8 @@ TInt >> baseSort [
 TInt >> printOn: aStream [
 	aStream nextPutAll: 'TInt'
 ]
+
+{ #category : #'α-renaming' }
+TInt >> uniq2: α [
+	"Nothing to do"
+]
diff --git a/src/SpriteLang/TRAll.class.st b/src/SpriteLang/TRAll.class.st
index 659bfc2b2..20afb4c27 100644
--- a/src/SpriteLang/TRAll.class.st
+++ b/src/SpriteLang/TRAll.class.st
@@ -139,3 +139,10 @@ go (TRAll p t)      = TRAll  (goP p) (go t)
 		r: (r tsubstGoP: t′ tVar: a)
 		t: (t tsubstGo: t′ tVar: a)
 ]
+
+{ #category : #'α-renaming' }
+TRAll >> uniq2: α [
+
+	self shouldBeImplemented
+
+]
diff --git a/src/SpriteLang/TVar.class.st b/src/SpriteLang/TVar.class.st
index 7b633bf85..8206d539b 100644
--- a/src/SpriteLang/TVar.class.st
+++ b/src/SpriteLang/TVar.class.st
@@ -77,3 +77,12 @@ TVar >> unifyV: t [
 	symbol nonRigid ifTrue: [ t assign: self.  ^t ].
 	self shouldBeImplemented.
 ]
+
+{ #category : #'α-renaming' }
+TVar >> uniq2: α [
+	| symbol′ |
+
+	symbol′ := α at: symbol ifAbsent:[ ^self ].
+	^self class symbol: symbol′
+
+]
diff --git a/src/SpriteLang/UnknownReft.class.st b/src/SpriteLang/UnknownReft.class.st
index 366d049fd..1531ed58f 100644
--- a/src/SpriteLang/UnknownReft.class.st
+++ b/src/SpriteLang/UnknownReft.class.st
@@ -69,3 +69,9 @@ UnknownReft >> substf: f [
 UnknownReft >> syms [
 	^#()
 ]
+
+{ #category : #'α-renaming' }
+UnknownReft >> uniq2: α [
+	"Nothing to do"
+
+]
diff --git "a/src/SpriteLang/\316\233Base.class.st" "b/src/SpriteLang/\316\233Base.class.st"
index 3226d0609..92dfd90e2 100644
--- "a/src/SpriteLang/\316\233Base.class.st"
+++ "b/src/SpriteLang/\316\233Base.class.st"
@@ -38,3 +38,10 @@ RType where r=Reft, here Reft meaning ΛReft.
 ΛBase >> freeTVarsGoB [
 	^Set new
 ]
+
+{ #category : #'α-renaming' }
+ΛBase >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self subclassResponsibility.
+]
diff --git "a/src/SpriteLang/\316\233EApp.class.st" "b/src/SpriteLang/\316\233EApp.class.st"
index 9a3bb8872..603ba1b00 100644
--- "a/src/SpriteLang/\316\233EApp.class.st"
+++ "b/src/SpriteLang/\316\233EApp.class.st"
@@ -103,3 +103,10 @@ cf. Parser.hs
 	cy := y checkImm: Γ rtype: s.
 	^{ ce & cy . t substImm: x imm: y }
 ]
+
+{ #category : #'α-renaming' }
+ΛEApp >> uniq2: α [
+	^self class
+		expr: (expr uniq2: α)
+		imm: (imm uniq2: α)
+]
diff --git "a/src/SpriteLang/\316\233Expression.class.st" "b/src/SpriteLang/\316\233Expression.class.st"
index 2d3b35b66..e5f55de19 100644
--- "a/src/SpriteLang/\316\233Expression.class.st"
+++ "b/src/SpriteLang/\316\233Expression.class.st"
@@ -157,6 +157,13 @@ cf. Elaborate.hs
 	^self goSubsTyExpr: su 
 ]
 
+{ #category : #'α-renaming' }
+ΛExpression >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self subclassResponsibility.
+]
+
 { #category : #'well-formedness' }
 ΛExpression >> wfExpr: γ sort: t [
 "
diff --git "a/src/SpriteLang/\316\233Reft.class.st" "b/src/SpriteLang/\316\233Reft.class.st"
index 0602c94b0..f0afc3752 100644
--- "a/src/SpriteLang/\316\233Reft.class.st"
+++ "b/src/SpriteLang/\316\233Reft.class.st"
@@ -75,3 +75,10 @@ freshR :: F.SrcSpan -> Env -> F.Sort -> Reft -> CG Reft
 	"instance F.Subable Reft where..."
 	self subclassResponsibility
 ]
+
+{ #category : #'α-renaming' }
+ΛReft >> uniq2: α [
+	"α-rename all variables. Returns a copy of receiver with all names unique."
+
+	self subclassResponsibility.
+]
diff --git "a/src/SpriteLang/\316\261Renames.class.st" "b/src/SpriteLang/\316\261Renames.class.st"
new file mode 100644
index 000000000..b22bcc65b
--- /dev/null
+++ "b/src/SpriteLang/\316\261Renames.class.st"
@@ -0,0 +1,97 @@
+Class {
+	#name : #'αRenames',
+	#superclass : #Object,
+	#instVars : [
+		'key',
+		'value',
+		'rest'
+	],
+	#classVars : [
+		'Sentinel'
+	],
+	#category : #'SpriteLang-Parsing'
+}
+
+{ #category : #'instance creation' }
+αRenames class >> empty [
+	^Sentinel
+]
+
+{ #category : #initialization }
+αRenames class >> initialize [
+	Sentinel := self basicNew
+]
+
+{ #category : #'instance creation' }
+αRenames class >> key: key value: value rest: rest [
+	^self basicNew key: key value: value rest: rest
+]
+
+{ #category : #'instance creation' }
+αRenames class >> new [
+	self shouldNotImplement. "Use #empty or #key:value:rest:"
+]
+
+{ #category : #accessing }
+αRenames >> at: anObject [
+	^self at: anObject ifAbsent:[ KeyNotFound signalFor: anObject ].
+
+]
+
+{ #category : #accessing }
+αRenames >> at: anObject ifAbsent: aBlock [
+	self == Sentinel ifTrue:[
+		^aBlock value
+	].
+
+	key = anObject ifTrue:[
+		^value
+	].
+
+	^rest at: anObject ifAbsent: aBlock
+
+
+]
+
+{ #category : #accessing }
+αRenames >> extMap: original to: unique [
+	"Extend current α-renames with new mapping.
+	 Return new α-renames."
+
+	^self class key: original value: unique rest: self.
+]
+
+{ #category : #GT }
+αRenames >> gtInspectorItemsIn: composite [
+	<gtInspectorPresentationOrder: 0>
+	^ composite fastTable
+		title: 'Renames';
+		display: [
+			| items |
+
+			items := Dictionary new.
+			self keysAndValuesDo: [ :k :v |
+				items at: k ifAbsentPut: v
+			].
+			items associations.
+		];
+		column: 'Key' evaluated: [ :each | GTObjectPrinter asTruncatedTextFrom: each key ];
+		column: 'Value' evaluated: [ :each | GTObjectPrinter asTruncatedTextFrom: each value ];
+		yourself.
+]
+
+{ #category : #initialization }
+αRenames >> key: keyArg value: valueArg rest: restArg [
+	key := keyArg.
+	value := valueArg.
+	rest := restArg
+
+]
+
+{ #category : #enumerating }
+αRenames >> keysAndValuesDo: aBlock [
+	self ~~ Sentinel ifTrue:[
+		aBlock value: key value: value.
+		rest keysAndValuesDo: aBlock
+	]
+]