Goal:
    A : Type  B : Type  C : Type  g : nat → A → B  f : nat → B → C
  ============================
   (nat → [] = [])


DEBUG:Going to execute:
congruence