RafaelBocquet

Require Import Equations.Equations.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Classes.EquivDec.
Require Import Program.

Ltac simpl_exist :=
  repeat (
      repeat match goal with
               | [ H : existT ?a ?b _ = existT ?a ?b _ |- _] =>
                 apply inj_pair2 in H