coq - coqで定理を証明しながら「false = true」命題に対処する方法

Question

私はcoqが初めてで、この定理を証明しようとしています

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

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

これがイコールの定義です

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.

これがこれまでの私の解決策です

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

そして、私はこのようなものになります

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

この出力は、定理が正しくなければならない場合、命題「偽 = 真」から命題「Var 0 = Var (S n)」が従う必要があることを意味することを理解していますが、どうすればよいかわかりません。私の証明を先に。