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