chris martensintentionally vague question; please document your assumptions in answers :)
from a (known valid) proof, (when) can you infer what theorem it proves?
(when) can a single proof prove multiple different theorems?
if you’re used to thinking of propositions and types interchangeably, try to wear your logician or mathematician hat for this question rather than leaning on intuitions about type systems. i’m curious whether that might lead to different places.
putting the question another way: imagine your friend looks up a proof of their favorite theorem in a textbook. they cover up the statement of the theorem and send it to you (who is well-versed in the relevant terminology used in the body of the proof, but has never seen this particular proof). can you guess the theorem?
Paul Khuong@chrisamaphone I'm tempted to claim that's necessary for a *good* proof. I think I usually wouldn't be able to recover the theorem from most proofs though :/