Equivalence of physical faces and corner matching

theorem MacMahon.face_corner_equivalence (i j : Label) : i ≠ j → ∀ (p : Pair) (k : Slot), HasCorner p (cornerAt i j k) ↔ ∃ (r : Fin 24), FaceFits (i, j) p k r

theorem MacMahon.builds_iff_physical (a : Inventory) (i j : Label) (h : i ≠ j) : Builds a (i, j) ↔ PhysicalBuilds a (i, j)

Corner matching is exactly matching the exposed faces by proper rotations.

theorem MacMahon.universal_iff_physical (a : Inventory) : Universal a ↔ PhysicalUniversal a