`done` loops because it repeatedly applies `split`
For example:
From stdpp Require Import streams.
Lemma foo (x y : stream nat) : x ≡ y.
Proof. done. (* loops *)
Is there any sensible way of only letting it apply split
for the case of inductive types (rather than also coinductive types)?
Or are there alternatives to avoid this?