Goal:
  
  A : Type
  P : nat → A → Type
  f : nat → A → A
  n : nat
  H : ∀ (n : nat) (x : A), P n x → f n x = x
  ============================
   ([] = [])


DEBUG:Going to execute:
assert X2
Level 1: evaluation returns
assert X2; [ exact (id0 id1) | clear id0 ]
where
id1 := n
of type
intropattern
id0 := f
of type
intropattern
flags := 
of type
tauto_flags
X2 := A → A
of type
constr of type tacvalue