This adds a regression test for #21871 (closed), which was fixed by the No Skolem Info rework (MR !7105 (closed)).