@@ -1141,15 +1141,6 @@ isInjective (Bind _ (Pi _ _ _ _) sc) = True
1141isInjective (App _ f a) = isInjective f
1141isInjective (App _ f a) = isInjective f
1142isInjective _ = False
1142isInjective _ = False
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
1153-- | Replace the outermost (index 0) de Bruijn variable with the given term
1144-- | Replace the outermost (index 0) de Bruijn variable with the given term
1154instantiate :: TT n -> TT n -> TT n
1145instantiate :: TT n -> TT n -> TT n
1155instantiate e = subst 0 where
1146instantiate e = subst 0 where