How to strengthen the induction hypothesis in the proof of Coq?

I am trying to formalize the application of context-free grammars in practice. I am having trouble proving one lemma. I tried to simplify my context to describe the problem, but this is still a bit cumbersome.

So, I have defined CFG in Chomsky normal form and terminal list output as follows:

Require Import List.
Import ListNotations.

Inductive ter : Type := T : nat -> ter.
Inductive var : Type := V : nat -> var.
Inductive eps : Type := E : eps.

Inductive rule : Type :=
  | Rt : var -> ter -> rule
  | Rv : var -> var -> var -> rule
  | Re : var -> eps -> rule.

Definition grammar := list rule.

Inductive der_ter_list : grammar -> var -> list ter -> Prop :=
  | Der_eps : forall (g : grammar) (v : var) (e : eps),
      In (Re v e) g -> der_ter_list g v []
  | Der_ter : forall (g : grammar) (v : var) (t : ter),
      In (Rt v t) g -> der_ter_list g v [t]
  | Der_var : forall (g : grammar) (v v1 v2 : var) (tl1 tl2 : list ter),
      In (Rv v v1 v2) g -> der_ter_list g v1 tl1 -> der_ter_list g v2 tl2 ->
        der_ter_list g v (tl1 ++ tl2).

      

        
        
        
      

    

I have objects that store a terminal and additional information, for example:

Inductive obj : Set := Get_obj : nat -> ter -> obj.

      

        
        
        
      

    

And I'm trying to figure out all the possible object lists that are derived from a given nonterminal (with helper functions):

Fixpoint get_all_pairs (l1 l2 : list (list obj)) : list (list obj) := match l1 with
    | [] => []
    | l::t => (map (fun x => l ++ x) l2) ++ get_all_pairs t l2
  end.

Fixpoint getLabels (objs : list obj) : list ter := match objs with
    | [] => []
    | (Get_obj yy ter)::t => ter::(getLabels t)
  end.

Inductive paths : grammar -> var -> list (list obj) -> Prop :=
  | Empty_paths : forall (g : grammar) (v : var) (e : eps),
      In (Re v e) g -> paths g v [[]]
  | One_obj_path : forall (g : grammar) (v : var) (n : nat) (t : ter) (objs : list obj),
      In (Rt v t) g -> In (Get_obj n t) objs -> paths g v [[Get_obj n t]]
  | Combine_paths : forall (g : grammar) (v v1 v2 : var) (l1 l2 : list (list obj)),
      In (Rv v v1 v2) g -> paths g v1 l1 -> paths g v2 l2 -> paths g v (get_all_pairs l1 l2).

      

        
        
        
      

    

(Each constructor paths

actually corresponds to a constructor rule

)

And now I'm trying to prove a fact about by paths

induction that every element of paths

can be inferred from a nonterminal:

Theorem derives_all_path : forall (g: grammar) (v : var)
  (ll : list (list obj)) (pths : paths g v ll), forall (l : list obj),
        In l ll -> der_ter_list g v (getLabels l).
Proof.
  intros g v ll pt l contains.
  induction pt.

      

        
        
        
      

    

This construction generates 3 subcells, 1st and 2nd, which I proved using constructors Der_eps

and Der_ter

respectively. But the context in the third subgoal is irrelevant to the proof of my goal, it has:

contains : In l (get_all_pairs l1 l2)
IHpt1 : In l l1 -> der_ter_list g v1 (getLabels l)
IHpt2 : In l l2 -> der_ter_list g v2 (getLabels l)

      

        
        
        
      

    

So, contains

means that l

is a concatenation of some elements from l1

and l2

, but putting in IHpt1

and IHpt2

is true if if l2

and l1

has empty lists, which is generally not true, so it is impossible to prove the purpose in this context.

The problem can be solved if l

in contains

, IHpt1

, IHpt2

will have different lists, but unfortunately, I do not know how to explain it to Coq. In any way in any way alter IHpt1

and IHpt2

to prove the purpose or any other way to prove the whole fact?

I tried to look paths_ind

, but that didn't make me happy.