coq - ツリー構造上の Coq での誘導

Question

これは非常に初歩的な質問であり、申し訳ありませんが、次の定理を証明するために Coq を使用しようとしてきましたが、その方法を理解できないようです。

(* Binary tree definition. *)
Inductive btree : Type := 
  | EmptyTree
  | Node : btree -> btree -> btree.
(* Checks if two trees are equal. *)

Fixpoint isEqual (tree1 : btree) (tree2 : btree) : bool :=
  match tree1, tree2 with
    | EmptyTree, EmptyTree => true
    | EmptyTree, _ => false
    | _, EmptyTree => false
    | Node n11 n12, Node n21 n22 => (andb (isEqual n11 n21) (isEqual n12 n22))
end.

Lemma isEqual_implies_equal : forall tree1 tree2 : btree, 
(isEqual tree1 tree2) = true -> tree1 = tree2.

私がやろうとしているのは、tree1 に続いて tree2 に誘導を適用することですが、これは実際には正しく機能しません。誘導を両方に同時に適用する必要があるようですが、方法がわかりません。