Require Import γδ.