Commit 2021-10-31 01:33 c9520174

chore(logic/embedding): docs, fixes (#10047)

• generalize function.extend and some lemmas from Type* to Sort*.
• add missing docs in logic.embedding;
• swap function.embedding.arrow_congr_left and function.embedding.arrow_congr_right;
• use function.extend to define the new function.embedding.arrow_congr_left.