Goal:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  ============================
   (eq_refl = eq_refl)


DEBUG:Going to execute:
match goal with
           | |- context [ inj_right_sigma ?P ?y ?y' _ ] =>
                 rewrite -> (inj_right_sigma_refl x P y)
           | |-
             context [ DepElim.simplification_sigma2_uip ?p ?x ?y ?X eq_refl ]
             =>
                 rewrite -> (DepElim.simplification_sigma2_uip_refl p x X);
                  simpl
           | |-
             context [ DepElim.simplification_sigma2_dec_point 
                         ?p ?x ?y ?X eq_refl ] =>
                 rewrite
                  -> (DepElim.simplification_sigma2_dec_point_refl p x X);
                  simpl
           | |- context [ DepElim.simplification_K_uip ?x ?p eq_refl ] =>
                 rewrite -> (DepElim.simplification_K_uip_refl x p);
                  simpl eq_rect
           | |- context [ DepElim.simplify_ind_pack ?B ?x ?p _ ?G _ eq_refl ]
             => rewrite -> (DepElim.simplify_ind_pack_refl B x p G _)
           | |-
             context [ DepElim.simplified_ind_pack 
                         ?B ?x ?p ?G
                         (DepElim.simplify_ind_pack_inv _ _ _ _ ?t) ] =>
                 rewrite -> (DepElim.simplify_ind_pack_elim B x p G t)
           end