@rahulc29 @antidote @isAdisplayName There are two instances of this problem in Lean, one easy to fix (or maybe already fixed?) and one harder to fix now without impacting a lot of library code. The latter is the ability to do recursion on proofs of proof irrelevant inductive propositions; if it was required to be proof relevant, the problem would disappear. But I think it can be hard to make this change, when considering the potential impacts on Lean code in the wild.
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View rahulc29@mathstodon.xyz profile | View antidote@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).