#[...]
The new notation should be use to input long sequences. Closes #1755
induct
to_unfold
simplify
simp*