A module with general theoremss
revEq : a = b -> b = a
Equality is symmetric
exfalso : Void -> a
From falsehood, anything follows a.k.a the principle of explosion