Goal:
  
  A : Type
  B : Type
  C : Type
  f : A -> B -> C
  g : A -> B -> C
  Hfg : f =2 g
  y : A
  y0 : B
  ============================
   (g y y0 = g y y0)


DEBUG:Going to execute:
easy

COQC theories/MCReflect.v