Structural subtyping for inductive types with functorial equality rules