Implement proof irrelevance, which is removing duplicate types of type proposition. Specifically:
add a new constant called prop
search for duplicate dtypes in names with definitions of types of type proposition in the rebuild method
remove these from context
Tests
tested manually on nats.p for "leq_trans"
proof irrelevance unit test
NOTE: one test case, parse_and_format_terms does not pass, but this is not related to proof irrelevance – it does not pass on main as well (an issue has been opened about this)
Description
Implement proof irrelevance, which is removing duplicate types of type proposition. Specifically:
rebuildmethodTests
NOTE: one test case,
parse_and_format_termsdoes not pass, but this is not related to proof irrelevance – it does not pass on main as well (an issue has been opened about this)