Simplify the equation
h using injectivity of constructors. See
injection_with. Returns the hypotheses that were added to the context, or an
empty list if the goal was solved by contradiction.
Simplifies equations in the context using injectivity of constructors. For
h : C x₁ ... xₙ = D y₁ ... yₘ in the context, where
are constructors of the same data type,
injections_with does the following:
C = D, it adds equations
x₁ = y₁, ...,
xₙ = yₙ.
C ≠ D, it solves the goal by contradiction.
injection_with for details, including information about
injections_with also recurses into the new equations
xᵢ = yᵢ. If it has to
recurse more than five times, it fails.