0 | ||| A module with general theoremss
 1 | module Theory.General
 2 |
 3 | ||| Equality is symmetric
 4 | total
 5 | export
 6 | revEq : a = b -> b = a
 7 | revEq Refl = Refl
 8 |
 9 | ||| From falsehood, anything follows
10 | ||| a.k.a the principle of explosion
11 | total
12 | export
13 | exfalso : Void -> a
14 | exfalso v = case v of {}
15 |
16 |