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