I also took the liberty of giving a specific error to iDestruct "H" as "[H1 H2 H3]", because that was the actual mistake I made (I wrote iDestruct "H" as "[$H1 H2]" because I keep wanting to name the thing I'm framing, but of course that doesn't really make sense).