"Split atomic pattern" for lambda parameters

[marat-rkh]

\func lemma (p : ∃ {x} (x = 0)) : ∃ {x} (x = 1) => TruncP.map p (\lam q => {?})

Since Arend 1.7 "Split atomic pattern" should be suggested for q here.