{α : Type u} →
  [inst : LE α] →
    [inst_1 : LT α] →
      {β : Type v} →
        [inst_2 : LE β] →
          [inst_3 : LT β] →
            [inst_4 : Std.PRange.UpwardEnumerable β] →
              [inst_5 : Std.PRange.LawfulUpwardEnumerable β] →
                [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] →
                  [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] →
                    [m : HasModel✝ α β] → [Std.Rxc.HasSize β] → Std.Rxc.HasSize α