`done` loops because it repeatedly applies `split`
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?