Transitivity in coercive subtyping
subtyping in dependent type theories with inductive types
scientific article; zbMATH DE number 2167399
scientific article