Hello, The https://plfa.github.io/Induction Page mentions the _≡⟨_⟩_ operator, which I couldn’t find on https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html Does it have an existing equivalent in the Standard Library? Cheers, Philippe PS My apologies if this question has already been asked on this list