Library Equations.TransparentEquations
This module sets the set constants of Equations to transparent mode so
that computation is possible inside Coq.
From Equations Require Import DepElim.
Global Transparent
simplification_sigma2_dec
simplification_sigma2_dec_point
simplification_K_dec
simplify_ind_pack simplified_ind_pack Id_simplification_sigma2.