This file introduces some of the new features of Coq 8.6

Multi-goal, multi-success typeclasses eauto engine

pred1 has priority over pred0

There is not pred2 1 instance

The resolution can backtrack across goals,

Here using two different calls to resolution on two different goals, using the multiple successes of the first call to find pred0

Here using a multi-goal call

Goal selectors

Applies the multi-goal tactic to the list of goals

Irrefutable patterns in binders

Keyed Unification

The purpose of Keyed Unification is to allow rewrite to see subterms to rewrite up to controlable reduction. The strategy is to match the lhs or rhs of the lemma with a subterm in the goal or hypothesis, by finding an applicative subterm whose head is equivalent to the head in the lemma and the use full unification on the arguments, whether they are closed or not.

Found no subterm matching g 0 in the current goal.

Now f and g are considered equivalent heads for subterm selection

Unification constraint handling

This option governs the automated solving of remaining unification constraints at each ".". Unification can use heuristics to solve these remaining constraints.

This higher-order unification constraint does not have a unique solution.

This lets the constraint float.

This forces constraint solving, here failing

If we remove the spurious dependency of the predicate on n: