Iris data structures

The paper Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic talks about defining "Iris Inductives". I think this would be a great feature to add to core Iris-Lean. Here's an illustrative example from the paper translated into Lean-y syntax:

iinductive IsListWithTail (tl : loc) : loc → list val → iProp GF where
  | nil : tl ↦ NIL -∗ IsListWithTail tl tl []
  | cons {v vs l l'} : l ↦ CONS (v,#l') -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l (v :: vs)
  | del {vs l l'} : l ↦ #l' -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l vs

I think we have all the theory for this, though getting an iinductive which behaves like a Lean inductive includes plenty of corner cases that would need some care. I'm similarly curious if we might be able to write a nice version of istructure-- I'd expect that to be a lot easier.

Start by reading the linked paper's discussion of Iris Inductives and comparing its illustrative iinductive syntax with the existing Iris-Lean implementation. The issue names no files or tests, so first locate the definitions and elaboration entry points for related core constructs. Done would require an agreed scope for iinductive, including its corner cases, and corresponding validation; istructure is presented as a separate possible feature.