summaryrefslogtreecommitdiff
path: root/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda
AgeCommit message (Expand)Author
2021-04-29Finally prove that e [ μ e / zero ] ≈ μ e.Chloe Brown