Goal:
  
  A : Type
  B : Type
  f : nat → A → B
  g : nat → A → B
  n : nat
  Hfg : ∀ (k : nat) (x : A), n ≤ k → k < #|[]| + n → f k x = g k x
  ============================
   ([] = [])


DEBUG:Going to execute:
congruence