on 22bcbd3 help sign in
1 file
../ Equality.idradd proof of `decEq x x = Yes Refl`