Basic rules of inference written up in Idris.
Just a little bit of syntactical sugar to make Idris theorems look more like Coq ones, sometimes when writing a proof that is not intended to be part of the program, but rather just for verification of properties, , its just kind of nice to have it look like a conventional proposition.