Function minitt::check::subtype::check_subtype_sum

pub fn check_subtype_sum(
    index: u32, 
    tcs: TCS, 
    sub_tree: BTreeMap<String, Box<Case>>, 
    super_tree: BTreeMap<String, Box<Case>>
) -> TCM<TCS>

Extracted from check_subtype to reduce indentation (but this function requires improvements).

Usually people want to recursively call check_subtype, but it's gonna cause stack-overflow if the sum type is recursive (like nat). To prevent this, I tried to call compare_normal before recursively check.
I'm not sure if this recursion is actually needed.

A bug report is expected to prove this to be false.