Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
CxTrans : forall {n m o} {De : Cx n} {De' : Cx m} {De'' : Cx o}
(p : n ≤′ m)
(q : m ≤′ o)
CxLe p De De'
CxLe q De' De''
CxLe (ℕtrans p q) De De''
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment