>Then it already knows how that made the proof work..

I think you cannot assume so, because pattern matching is not reasoning.