`dec_trivial`:1024 := of_is_true trivial