Commit 2024-02-20 03:48 410db900
View on Github →fix(Logic/Embedding/Basic): Generalise arrowCongrRight_apply (#10739)
f does not need to be an embedding, and this version is syntactically strictly more general.
fix(Logic/Embedding/Basic): Generalise arrowCongrRight_apply (#10739)
f does not need to be an embedding, and this version is syntactically strictly more general.