Intermediate Type from Left

Considering examples like

mu a. Top -> (mu b. B1)
<:
mu a. Top -> (mu b. B2)
(but not mu a. a -> (mu b. B1))
<:
mu a. a -> (mu b. B2)

We might based our reasoning on the left:

given
  A1 [a- |-> {a : A1}]
& A2 [a- |-> {a : A2}]
& A3 [a- |-> {a : A3}]
<<
  B1 & B2 [a- |-> {a : B}]

we can case on whether
A1 [a- |-> {a : A1 & A2 & A3}]
& A2 [a- |-> {a : A1 & A2 & A3}]
& A3 [a- |-> {a : A1 & A2 & A3}]
is a subtype of 
B1 & B2 [a- |-> {a : B}]


B = mu a. a -> (mu b. (
  b -> Int & 
  b -> Bool
))

[ a.  {a : ..... } -> [ b. 
	  {b : b -> Int & b -> Bool} -> Int 
	& {b : b -> Int & b -> Bool} -> Bool
  ]  
]

A can be:
-- refl
  mu a. a -> (mu b. (b -> Int & b -> Bool)) 
-- mu a. a -> XXX & mu a. a -> XXX
  ...
-- mu a. Top -> XXX
  mu a. Top -> (mu b. (b -> Int & b -> Bool)) 
  mu a. Top -> (mu b. (Top -> Int & b -> Bool))
  mu a. Top -> ((mu b. b -> Int) & (mu b. b -> Bool)))
-- mu a. Top -> XXX & mu a. Top -> XXX
  (mu a. Top -> (mu b. b -> Int)) & (mu a. Top -> (mu b. b -> Bool))
  (mu a. Top -> (mu b. b -> Int)) & (mu a. Top -> (mu b. Top -> Bool))
For this left type, no mu-split of the right type can satisfy being a supertype of A1/A2

  [a. Top -> [b. {b : b -> Int } -> Int ] ]
& [a. Top -> [b. {b : b -> Bool } -> Bool ] ]
==
  [a. Top -> [b. 
	  {b : b -> Int } -> Int 
	& {b : b -> Bool } -> Bool
  ] 
]
<<
[a. {a. .... } -> [b. 
	  {b : b -> Int } -> Int 
	& {b : b -> Bool } -> Bool
  ] 
]



[a. A1 [{a : A1}/a-] ] & [a. A2 [{a : A2}/a-] ] << [a. B [{a: B}/a-]]
==
[a. A1 [{a : A1}/a-] & A2 [{a : A2}/a-] ]
(1) when a is not in fv_neg(A1) and fv_neg(A2)
  == [a. A1 [{a : A1 & A2 }/a-] & A2 [{a : A1 & A2}/a-] ]
  == [a. (A1 & A2) [ {a : A1 & A2} /a- ] ] << [a. B [{a: B}/a-]] OK


[a. A1 [{a : A1}/a-] & A2 [{a : A2}/a-] ] << [a. B [{a: B}/a-]]
(2) when a is in fv_neg(A1)

     which implies a negative reflexive comparison in A1 with B,  
     we know A1 & A2 << B << A1

(2.1) when a is in fv_neg(A1), a is not in fv_neg(A2)


e.g. A1 & A2 << B << A1 can be:
(a -> Int) & (Top -> a) << (a -> Int) & (Bool -> a) << (a -> Int)?

we want to argue:
  mu a. a -> Int 
& mu a. Top -> a
<:
  mu a. a -> Int 
& mu a. Bool -> a <--- How to find? based on a not in fv_neg(A2)
<:
  mu a. ( a -> Int ) & ( Bool -> a )

or even more complex:
e.g. A1 & A2 << B << A1 can be:
   a -> [b. {b : b -> Bool} -> Bool]
 & Top -> [b. {b : b -> Int} -> Int ]  
<< a -> [b. {b : b -> Bool} -> Bool]
 & a -> [b. {b : b -> Int} -> Int ]
<< a -> [b. ({b : b -> Bool} -> Bool) & ({b : b -> Int} -> Int) ]
(but not
   a -> [b. ({b : b -> Bool & b -> Int} -> Bool) 
          & ({b : b -> Bool & b -> Int} -> Int) ]
 as it will break the [B << A1] constraint
)
<< a -> [b. {b : b -> Bool} -> Bool]