Require Export Bool Lia List Setoid Morphisms Arith.
From Undecidability.Shared.Libs.PSL Require Export Tactics.
Require Import FinFun.

Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Records.
Global Unset Printing Implicit Defensive.

Notation injective := FinFun.Injective.
Notation surjective := FinFun.Surjective.