theorem TwoPeopleDifferingInWealth.mk.injEq
theorem TwoPeopleDifferingInWealth.mk.injEq
: ∀ (p1 p2 : nwtxrh89.Person) (p1Character p2Character : n82pf9zy.MoralCharacter)
  (p1_is_rich : qfqvcx4c.Rich (Subtype.val p1)) (p2_is_not : ¬qfqvcx4c.Rich (Subtype.val p2))
  (p1_has_character : n82pf9zy.HasMoralCharacter (Subtype.val p1) (Subtype.val p1Character))
  (p2_has_character : n82pf9zy.HasMoralCharacter (Subtype.val p2) (Subtype.val p2Character))
  (all_else_equal : qfqvcx4c.SameCircumstancesExceptWealth (Subtype.val p1) (Subtype.val p2))
  (p1_1 p2_1 : nwtxrh89.Person) (p1Character_1 p2Character_1 : n82pf9zy.MoralCharacter)
  (p1_is_rich_1 : qfqvcx4c.Rich (Subtype.val p1_1)) (p2_is_not_1 : ¬qfqvcx4c.Rich (Subtype.val p2_1))
  (p1_has_character_1 : n82pf9zy.HasMoralCharacter (Subtype.val p1_1) (Subtype.val p1Character_1))
  (p2_has_character_1 : n82pf9zy.HasMoralCharacter (Subtype.val p2_1) (Subtype.val p2Character_1))
  (all_else_equal_1 : qfqvcx4c.SameCircumstancesExceptWealth (Subtype.val p1_1) (Subtype.val p2_1)),
  (qfqvcx4c.TwoPeopleDifferingInWealth.mk p1 p2 p1Character p2Character p1_is_rich p2_is_not p1_has_character
        p2_has_character all_else_equal =
      qfqvcx4c.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)