Estou tentando provar que, na minha opinião, é um teorema razoável:

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

A prova por indução chega ao ponto em que eu preciso provar isso:

lemma1 : (n : Nat) -> (n - 0) = n

É o que acontece quando tento provar (o lema, por uma questão de simplicidade) usando o provador interativo:

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

Eu senti que devia estar faltando algo sobre a definição de menos, então procurei na fonte:

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

A definição que eu preciso está aí!minus left Z = left. Meu entendimento era que Idris deveria apenas substituirminus m 0 comm aqui, e isso é então reflexivamente verdadeiro. O que eu perdi?