Let&#39;s say I&#39;m writing a proof with a goal type of:<div><br></div><div><div>Goal: (fromℕ</div><div>       (peanoInduction (λ {x&#39;} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)</div><div>        (toPeano (x ∷ xs)))</div><div>       | (.Data.Digit._.helper 0</div>
<div>          (peanoInduction (λ {x&#39;} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)</div><div>           (toPeano (x ∷ xs)))</div><div>          (peanoInduction (λ {x&#39;} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)</div><div>           (toPeano (x ∷ xs)))</div>
</div><div>  ...</div><div><br></div><div>Note that it will not proceed in normalizing the goal type unless I can match on the result of the expression after the pipe. Unfortunately, said expression lives within a where block in a module that&#39;s out of my control, so I can&#39;t see it at all, to proceed on the proof. As far as I can understand, assuming there aren&#39;t completely different approaches to the proof, this makes my proof actually impossible. Am I correct?</div>
<div><br></div><div>Now, the ._.helper notation looks like the helper is secretly living inside an anonymous module that the where block created. Given the recent change that made datatypes into modules, would it be worthwhile or problematic to make all value declarations with where blocks into explicit modules as well, so that we can open them and prove things about whatever happened inside? Would this cause problems in other ways?</div>
<div><br></div><div>Even if my suggestion isn&#39;t valid, it seems like it&#39;d be good to have a good answer for this kind of situation. Or is there already some solution that I&#39;m missing?</div><div><br></div><div>
Thanks,</div><div>Dan</div>