Small modification to collect the level params in more cases.
This eliminates some errors in simulations via the Repl. E.g. the simulation of the following theorem:
theorem exists_not_acc_lt_of_not_acc {a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a := by
contrapose! h
refine' ⟨_, fun b hr => _⟩
by_contra hb
exact h b hb hr
#align rel_embedding.exists_not_acc_lt_of_not_acc RelEmbedding.exists_not_acc_lt_of_not_acc
would throw an error that a level param does not exist.
Small modification to collect the level params in more cases.
This eliminates some errors in simulations via the Repl. E.g. the simulation of the following theorem:
would throw an error that a level param does not exist.