Face and corner matching for targets in tableau row 2

theorem MacMahon.face_corner_20 (p : Pair) (k : Slot) : HasCorner p (cornerAt 2 0 k) ↔ ∃ (r : Fin 24), FaceFits (2, 0) p k r

theorem MacMahon.face_corner_21 (p : Pair) (k : Slot) : HasCorner p (cornerAt 2 1 k) ↔ ∃ (r : Fin 24), FaceFits (2, 1) p k r

theorem MacMahon.face_corner_23 (p : Pair) (k : Slot) : HasCorner p (cornerAt 2 3 k) ↔ ∃ (r : Fin 24), FaceFits (2, 3) p k r

theorem MacMahon.face_corner_24 (p : Pair) (k : Slot) : HasCorner p (cornerAt 2 4 k) ↔ ∃ (r : Fin 24), FaceFits (2, 4) p k r

theorem MacMahon.face_corner_25 (p : Pair) (k : Slot) : HasCorner p (cornerAt 2 5 k) ↔ ∃ (r : Fin 24), FaceFits (2, 5) p k r