Lean Kernel Arena / tutorial/113_indexedStructEta

Structure eta applies only to non-recursive structures without indices: the official kernel's is_non_rec_structure requires nindices == 0, so it does not fire for IndexedSingleton even though that has a single constructor.

Every field of IndexedSingleton.mk is a proof, so a kernel that checks only "has a single constructor" and then compares the fields against projections would have proof irrelevance discharge the remaining goals, and would wrongly accept this.