feat: notations for telescope arguments

[alvinylt]

Description

Addresses #672 (review).

Introduces the notations for Tele.nil, Tele.cons, Tele.Arg.nil and Tele.Arg.cons. The coercion is also ported.

The double bracket ⟦…⟧ is used instead of the single bracket […] for two reasons.

• We cannot use it directly in the theorem's type signature like this:

  theorem persistent_seq_wp_atomic {α : [tele] → IProp GF} {β : [tele] → TB.Arg → IProp GF} …

  This is because […] is parsed as a type class hypothesis.

• A workaround would be to add parentheses:

  theorem persistent_seq_wp_atomic {α : ([tele]) → IProp GF} {β : ([tele]) → TB.Arg → IProp GF} …

  The notations are elaborated correctly, so the theorem and its proof are accepted. Nonetheless, weird things happen as it conflates with the list notation, which results in tele and tele_arg being registered as implicit parameters.

  

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files