diff --git a/notes/interpretation-of-as-types.txt b/notes/interpretation-of-as-types.txt
deleted file mode 100644
index bf535c3b47..0000000000
--- a/notes/interpretation-of-as-types.txt
+++ /dev/null
@@ -1,47 +0,0 @@
-
-Two interpretations of types of the form T['a] as 'a
- - if interpreted as proper recursive (a.k.a., infinite) type,
-    it means ('a -> Bot) as 'a is too restrictive a type for self-app
-    (it's specialized for applying self-app to itself, resulting in non-term and the Bot type as expected),
-    but the original type ('a -> 'b) as 'a works fine.
-    explanation:
-      'b cannot be simplified away, because it appears in both pos and neg,
-      since 'a itself does (through its own recursive occurrence!)
- - if interpreted as a type variable bounded with its body accordingly to its position,
-    then ('a -> Bot) as 'a is STILL NOT an acceptable type for self-app
-    For instance, let's see what happens when we pass it (lam x. 42) of type Top -> Int;
-      we constrain ?a <: (Top -> Int) -> ?b for some fresh ?b, where ?a :> (?a -> Bot)
-      this leads to  (?a -> Bot)  <:  (Top -> Int) -> ?b
-      decomposed as  (Top -> Int) <: ?a  and  Bot <: ?b
-      which leads to  Top -> Int  <:  Top -> Int
-      So the constraints work out, but we end up with result type ?b where ?b :> Bot,
-      which is obviously wrong! (we should have gotten an Int)
-    And this also happens for the original type ('a -> 'b) as 'a,
-      which is however valid under the other interpretation!
-    Here, we may need to think harder about the phrase "bounded accordingly to its position"
-    Again, the position of 'a really is both pos and neg, so we should really interpret the type as
-      ?a :> ('a -> 'b) <: ('a -> 'b)
-    Under this revised interpretation, things work out when applying it to (lam x. 42):
-      we constrain ?a <: (Top -> Int) -> ?c for some fresh ?c, where ?a :> (?a -> ?b) <: (?a -> ?b)
-      this leads to  ?a -> ?b  <:  (Top -> Int) -> ?c
-      decomposed as  (Top -> Int) <: ?a  and  ?b <: Int
-      which leads to  Top -> Int  <:  Top -> Int  and  Top -> Int  <:  ?a -> ?b
-      decomposed as  ?a <: Top  and  Int <: ?b
-      which leads to  Int <: Int
-      So the constraints work out, and we do get the appropriate result type Int
-
-Conclusion:
-  Both interpretations of "T['a] as 'a" as infinite types and as type variables seem valid and equivalent.
-  We can treat "T['a] as 'a" as representing a type variable ?a upper and lower-bounded by T[?a].
-  In the particular case where it appears only positively (resp. neg.) in the original type AS WELL
-  AS in T[?a] itself, then we can forget about the lower bound (resp. upper bound).
-
-Note:
-  The bounds of a recursive types that appear both positively and negatively have no reason to be the same;
-  so our interpretation above is unlikely to capture the full generality of recursive type variables.
-  I have changed the type expansion algorithm to only produce recursive type variables which occur only
-  in positive or only in negative positions (the change was easy). Before that, the algorithm was probably
-  wrong anyways, under our both-bounds interpretation.
-  We'll no longer infer things like "('a -> 'b) as 'a", but rather "(('a -> 'b) -> 'b) as 'a",
-  which is easier to co-occurrence-analyze using the current infrastructure (otherwise, we'd have to keep
-  track of the fact some recursive variables may appear both posly and negly as we do the analysis!)