Subtyping + extensionality: Confluence of beta-eta top in Fsub, extended abstract