5 lines
251 B
Coq
5 lines
251 B
Coq
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.
|