Verify.Involutive_Heyting_Algebra
H : Interface.INVOLUTIVE_HEYTING_ALGEBRA
include sig ... end
val involution : H.t -> bool