∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Ring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommGroup E}
  {inst_3 : Module 𝕜 E} {faces : Set (Finset E)} {empty_notMem : ∅ ∉ faces}
  {indep : ∀ {s : Finset E}, s ∈ faces → AffineIndependent 𝕜 Subtype.val}
  {down_closed : ∀ {s t : Finset E}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces}
  {inter_subset_convexHull :
    ∀ {s t : Finset E}, s ∈ faces → t ∈ faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)}
  {faces_1 : Set (Finset E)} {empty_notMem_1 : ∅ ∉ faces_1}
  {indep_1 : ∀ {s : Finset E}, s ∈ faces_1 → AffineIndependent 𝕜 Subtype.val}
  {down_closed_1 : ∀ {s t : Finset E}, s ∈ faces_1 → t ⊆ s → t.Nonempty → t ∈ faces_1}
  {inter_subset_convexHull_1 :
    ∀ {s t : Finset E}, s ∈ faces_1 → t ∈ faces_1 → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)},
  { faces := faces, empty_notMem := empty_notMem, indep := indep, down_closed := down_closed,
        inter_subset_convexHull := inter_subset_convexHull } =
      { faces := faces_1, empty_notMem := empty_notMem_1, indep := indep_1, down_closed := down_closed_1,
        inter_subset_convexHull := inter_subset_convexHull_1 } →
    faces = faces_1