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