"Split atomic pattern" for lambda parameters #307
Description
\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.
{{ message }}
\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.