@@ -1141,15 +1141,6 @@ isInjective (Bind _ (Pi _ _ _ _) sc) = True
11411141isInjective (App _ f a) = isInjective f
11421142isInjective _ = False
11431143
1144−-- | Count the number of instances of a de Bruijn index in a term
1145−vinstances :: Int -> TT n -> Int
1146−vinstances i (V x) | i == x = 1
1147−vinstances i (App _ f a) = vinstances i f + vinstances i a
1148−vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
1149− where instancesB (Let c t v) = vinstances i v
1150− instancesB _ = 0
1151−vinstances i t = 0
1152−
11531144-- | Replace the outermost (index 0) de Bruijn variable with the given term
11541145instantiate :: TT n -> TT n -> TT n
11551146instantiate e = subst 0 where