Type soundness of functional languages with subtyping in Lang-n-Prove. - Matteo Cimini; Joan Montas (Sci. Comput. Program., 2026)