∀ {etaPoly inlinePartial implementedBy inlineDefs etaPoly_1 inlinePartial_1 implementedBy_1 inlineDefs_1 : Bool},
  { etaPoly := etaPoly, inlinePartial := inlinePartial, implementedBy := implementedBy, inlineDefs := inlineDefs } =
      { etaPoly := etaPoly_1, inlinePartial := inlinePartial_1, implementedBy := implementedBy_1,
        inlineDefs := inlineDefs_1 } →
    etaPoly = etaPoly_1 ∧ inlinePartial = inlinePartial_1 ∧ implementedBy = implementedBy_1 ∧ inlineDefs = inlineDefs_1