Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable.
From Hammer Require Import Tactics.
Require Import ssreflect ssrbool.
From stdpp Require Import relations (nsteps (..), rtc(..)).
Import Psatz.