Coq中valid_path归纳证明的归纳假设(IH)格式问题求助

在进行形式化证明时，证明path_equal引理遇到了归纳假设（IH）格式不正确的问题，具体情况如下：

问题说明 #

我需要证明从同一节点出发的有效路径是唯一的，但当前通过induction H0生成的归纳假设为：

IHvalid_path : valid_path ls xd (x :: p') → p'0 = x :: p'

而我实际需要的归纳假设形式应该是：

IHvalid_path : valid_path ls xd p'0 → valid_path ls xd p' → p'0 = p'

已经尝试过generalize方法，但仍无法解决问题，希望得到帮助。

相关代码 #

From stdpp Require Import mapset.

From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import proofmode.
From iris.heap_lang Require Export proofmode notation.

Definition Node : Type := nat.
Definition Children : Type := (loc * loc).
Definition Entry : Type := (Node * Children).

Definition ldd_state : Type := gmap loc (nat * (loc * loc)).

Definition ldd_zero : loc := Loc 0.
Definition ldd_one : loc := Loc 1.

(* Loc 0 and Loc 1 will never be present in the state.
   This is to prevent the true, false leaves having children and values. *)
Definition state_ok (ls : ldd_state) : Prop :=
  ls !! ldd_zero = None ∧ ls !! ldd_one = None.
    
Definition get_down (ls : ldd_state) (x : loc) : option loc := 
  ls !! x ≫= λ n, Some (snd n) ≫= λ n, Some (fst n).

Definition path := list loc.
Identity Coercion path_to_list : path >-> list.

Inductive valid_path (ls : ldd_state) (x : loc) : path → Prop :=
  | path_Et : x = ldd_one → valid_path ls x [ldd_one]
  | path_D  : ∀ (xd : loc) (p' : path),
      get_down ls x = Some xd → 
      valid_path ls xd p' → 
      valid_path ls x (x :: p').

Lemma path_equal : ∀ (ls : ldd_state) (x : loc) (p p' : path),
  state_ok ls → valid_path ls x p → valid_path ls x p' → p = p'.
intros. induction H0.
Proof.
- destruct H1.  + admit. (* easy case, this is contradiction *)
                + admit. (* again, easy contradiction *)
- destruct H1.  + admit. (* easy case, contradiction *)
                + (* Stuck here *)
 Admitted.

内容的提问来源于stack exchange，提问作者someStudentCS