Type soundness of functional languages with subtyping in Lang-n-Prove. ~ Matteo Cimini, Joan Montas. https://www.sciencedirect.com/science/article/abs/pii/S0167642325001194 #ITP #Abella