Extension of the Ltac2 standard library To use the library, require via the following command: Require Import bedrock.ltac2.extra.extra.