Type checking ./ott.idr ?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1) Z