Library Equations.OpaqueEquations
This module sets the set constants of Equations to opaque mode so
that computation is not possible inside Coq, the tactics need this
to solve obligations.
From Equations Require Import DepElim.
Global Opaque simplification_sigma2_dec
simplification_sigma2_dec_point
simplification_K_dec
simplify_ind_pack simplified_ind_pack Id_simplification_sigma2.