feat(logic/basic): add lemma `pi_congr` (#14616)
This lemma is used in #14153, where `congrm` is defined.
A big reason for splitting these 3 lines off the main PR is that they are the only ones that are not in a leaf of the import hierarchy: this hopefully saves lots of CI time, when doing trivial changes to the main PR.
