theorem TwoPeopleDifferingInWealth.mk.inj
theorem TwoPeopleDifferingInWealth.mk.inj
: ∀ {p1 p2 : azt4989z.Person} {p1Character p2Character : pv802k7b.MoralCharacter}
  {p1_is_rich : zk1mxe7x.Rich (Subtype.val p1)} {p2_is_not : ¬zk1mxe7x.Rich (Subtype.val p2)}
  {p1_has_character : pv802k7b.HasMoralCharacter (Subtype.val p1) (Subtype.val p1Character)}
  {p2_has_character : pv802k7b.HasMoralCharacter (Subtype.val p2) (Subtype.val p2Character)}
  {all_else_equal : zk1mxe7x.SameCircumstancesExceptWealth (Subtype.val p1) (Subtype.val p2)}
  {p1_1 p2_1 : azt4989z.Person} {p1Character_1 p2Character_1 : pv802k7b.MoralCharacter}
  {p1_is_rich_1 : zk1mxe7x.Rich (Subtype.val p1_1)} {p2_is_not_1 : ¬zk1mxe7x.Rich (Subtype.val p2_1)}
  {p1_has_character_1 : pv802k7b.HasMoralCharacter (Subtype.val p1_1) (Subtype.val p1Character_1)}
  {p2_has_character_1 : pv802k7b.HasMoralCharacter (Subtype.val p2_1) (Subtype.val p2Character_1)}
  {all_else_equal_1 : zk1mxe7x.SameCircumstancesExceptWealth (Subtype.val p1_1) (Subtype.val p2_1)},
  zk1mxe7x.TwoPeopleDifferingInWealth.mk p1 p2 p1Character p2Character p1_is_rich p2_is_not p1_has_character
        p2_has_character all_else_equal =
      zk1mxe7x.TwoPeopleDifferingInWealth.mk p1_1 p2_1 p1Character_1 p2Character_1 p1_is_rich_1 p2_is_not_1
        p1_has_character_1 p2_has_character_1 all_else_equal_1 →
    p1 = p1_1 ∧ p2 = p2_1 ∧ p1Character = p1Character_1 ∧ p2Character = p2Character_1