+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
+ when iseq uri ->
+ (let _,context,_ = env in
+ try
+ let s,m,_ =
+ Inference.unification m m context left right CicUniv.empty_ugraph
+ in
+ let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+ let m = Subst.apply_subst_metasenv s m in
+ Some (goalproof, reflproof, 0, s,m)
+ with _ -> None)