search

berenoguz / Math

Formalization of Mathematics using Type Theory of Agda Programming Language
GNU General Public License v3.0
11 stars 0 forks source link

Add diagonal inference of equality #4

Closed berenoguz closed 6 years ago

berenoguz commented 6 years ago

Add theorems such that a == b -> c == a -> b == c and so on. Not very essential, but helpful in proofs.

berenoguz commented 6 years ago

Unnecessary, transitive is enough.