on 385dcbf help sign in
2 lines 83 B history raw
1?prf : (x : Bool) -> (x1 : Bool) -> El (EQ Two x Two x1) -> El (EQ Two x Two x1)
2Z