We: Hey, find me TM and TRem such that exists SelectLeast[T, TM, TRem] where T defined by L = H :: T. And TM < H should hold.
1. hlistSelectLeast3 works since precedence
hlistSelectLeast3[H = _1, T = _2 :: _3 :: HNil, TM = ?, TRem = ?]: SelectLeast[H :: T, TM, H :: TRem]
We: Hey, find me TM2 and TRem2 such that exists SelectLeast[T2, TM2, TRem2] where T2 defined by T == H2 :: T2. And TM2 < H2 should hold.
2. hlistSelectLeast3 works since precedence
hlistSelectLeast3[H2 = _2, T2 = _3 :: HNil, TM2 = ?, TRem = ?]: SelectLeast[H2 :: T2, TM2, TRem2]
We: Hey, find me TM3 and TRem3 such that exists SelectLeast[T3, TM3, Trem3] where T3 defined by T2 == H3 :: TM3. And TM3 < H3 should hold.
3. hlistSelectLeast3 works since precedence
hlistSelectLeast3[H3 = _3, T3 = HNil, TM3 = ?, TRem3 = ?]: SelectLeast[H3 :: T3, TM3, Trem3]
We: Hey, find me TM4 and TRem4 such that exists SelectLeast[T4, TM4, TRem4] where T4 defined by T3 == H4 :: TM4. And TM4 < H4 should hold.
4. Oops, T3 == H4 :: TM4 couldn't be evaluated since T3 is HNil, go to hListSelectLeast1
5. Oops hListSelectLeast1 requires T3 == TM4 :: T5, can't do that since T3 is HNil. Go 1 step back and then to hListSelectLeast1, thus forgetting T4, TM4, T5
6. Trying to find SelectLeast[T3, TM3, TRem3] such that T3 == TM3 :: TRem3
7. Oops T3 is HNil. Go 1 step back and then to hListSelectLeast1, thus forgetting T3, TM3, Trem3
8. Trying to find SelectLeast[T2, TM2, TRem2] such that T2 = TM2 :: TRem2
hListSelectLeast1[H = _3, T = HNil]
9. FOUND! Returning SelectLeast[L = _3 :: HNil, M = _3, Rem = HNil], so TM2 = _3, TRem2 = HNil. And TM2 < H2 becomes _3 < _2, oops, wrong! Go 1 step back and then to hlistSelectLeast1, thus forgetting T2, H2, TM2, TRem2
10. Trying to find SelectLeast[T, TM, TRem] such that T = TM :: TRem
hListSelectLeast1[H = _2, T = _3 :: HNil]
11. FOUND! Returning SelectLeast[L = _2 :: 3 :: HNil, M = _2, Rem = 3 :: HNil], so TM = _2, TRem = 3 :: _HNil. And TM < H becomes _2 < _1, oops, wrong! Go 1 steb back and then to hlistSelectLeast1, thus forgetting T, TM, TRem
12. Trying to find SelectLeast[L = _1 :: _2 :: _3 :: HNil, M, Rem] such that L = M :: Rem
hListSelectLeast1[H = _1, T = _2 :: _3 :: HNil]
13. FOUND! Returning SelectLeast[L = _1 :: _2 :: _3 :: HNil, M = _1, Rem = _2 :: _3 :: HNil]
14. Applying sl, returning (_1, _2 :: _3 :: HNil)