Expand description

Proof utilities

Traits