on dcdebfc help sign in
1 file
../ Equality.idrUse postulates for decEq primitive proofs