Given a local constant H : C x₁ ... xₙ = D y₁ ... yₘ, where C and D are
fully applied constructors, injection_with H ns base offset does the
If C ≠ D, it solves the goal (using the no-confusion rule).
If C = D (and thus n = m), it adds hypotheses
h₁ : x₁ = y₁, ..., hₙ : xₙ = yₙ to the local context. Names for the hᵢ
are taken from ns. If ns does not contain enough names, then the names
are derived from base and offset (by default h_1, h_2 etc.; see
Special case: if C = D and n = 0 (i.e. the constructors have no
arguments), the hypothesis h : true is added to the context.
injection_with returns the new hypotheses and the leftover names from ns
(i.e. those names that were not used to name the new hypotheses). If (and only
if) the goal was solved, the list of new hypotheses is empty.
Simplifies equations in the context using injectivity of constructors. For
each equation h : C x₁ ... xₙ = D y₁ ... yₘ in the context, where C and D
are constructors of the same data type, injections_with does the following:
If C = D, it adds equations x₁ = y₁, ..., xₙ = yₙ.
If C ≠ D, it solves the goal by contradiction.
See injection_with for details, including information about base and
injections_with also recurses into the new equations xᵢ = yᵢ. If it has to
recurse more than five times, it fails.