Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add
Data.List.Relation.Binary.Sublist.Setoid
categorical properties (…
…#2385) * refactor: `variable` declarations and `contradiction` * refactor: one more `contradiction` * left- and right-unit lemmas * left- and right-unit lemmas * `CHANGELOG` * `CHANGELOG` * associativity; fixes #816 * Use cong2 to save rewrites * Make splits for ⊆-assoc exact, simplifying the [] case * Simplify ⊆-assoc not using rewrite * Remove now unused private helper * fix up names and `assoc` orientation; misc. cleanup * new proofs can now move upwards * delegate proofs to `Setoid.Properties` --------- Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>
- Loading branch information