ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )