prueba: cómo lidiar con la proposición "falso = verdadero" al demostrar teoremas en coq

Soy nuevo en coq y estoy intentando demostrar este teorema

Inductive expression : Type :=
  | Var (n : nat)
.
.

Theorem variable_equality : forall x : nat, forall n : nat,
  ((equals x n) = true) -> (Var x = Var n).

Esta es la definición de iguales

Fixpoint equals (n1 : nat) (n2 : nat) :=
  match (n1, n2) with
    | (O, O)      => true
    | (O, S n)    => false
    | (S n, O)    => false
    | (S n, S n') => equals n n'
  end.

Esta es mi solución hasta ahora

Proof.
intros x n. induction x as [| x' IH].
  - destruct n. 
    + reflexivity.
    + simpl. intro. 

y termino con algo como esto

1 subgoal 
n : nat
H : false = true
-------------------------
Var 0 = Var (S n)

Entiendo que este resultado significa que la proposición "Var 0 = Var (S n)" debe seguirse de la proposición "falso = verdadero" si el teorema tiene que ser correcto, pero no sé qué hacer al respecto y seguir adelante con mi demostración.

------------------------------------

Otra opción, discrimina cuál es la táctica dedicada a este tipo de objetivos: se supone que resuelve exactamente este tipo de problemas.(es decir, igualdades de distintos constructores en sus hipótesis) y nada más.

Goal false = true -> False.
discriminate.
Qed.

Además, es un terminador, lo que significa que falla si el objetivo no se resuelve después de su uso, al contrario de la inversión y la congruencia que tendrán éxito en algunos casos en los que no resuelven el problema esperado y tienen éxito en un resultado "inesperado". ; camino.

por ejemplo

Goal true = true -> True.
inversion 1.
Qed.

y

Goal true = true -> S 1 = S 1.
congruence.
Qed.

Personalmente, uso by [] (que también es un terminador) de ssreflect para este tipo de objetivos y para todos los objetivos "triviales". objetivos del tipo:

Require Import ssreflect.

Goal false = true -> False.
by [].
Qed.

------------------------------------

Otra opción: en lugar de invertirion, usa la congruencia:

Goal false=true -> False.
  congruence.
Qed.

Esta táctica está dedicada a explotar la desunión de los constructores.

------------------------------------

Utilice la inversión en hipótesis como en:

Goal false=true -> False.
intros H.
inversion H.
Qed.