```tex \func lemma1 => (1, 2) \func lemma2 : Nat => \let p => lemma1 \in {?} ``` "Split atomic pattern" could be suggested for `p` here.