comment utiliser l'hypothèse qui inclut le quantificateur universel dans Coq?

Question

Je suis nouveau à Coq. Je suis confus au sujet de la preuve ci-dessous:

Lemma nth_eq : forall {A} (l1 l2 : list A), 
length l1 = length l2 -> 
(forall d k, nth k l1 d = nth k l2 d) ->l1 = l2. 
Proof. 
    intros. 

Le résultat montre:

1 subgoal 
A : Type 
l1, l2 : list A 
H : length l1 = length l2 
H0 : forall (d : A) (k : nat), nth k l1 d = nth k l2 d 
______________________________________(1/1) 
l1 = l2 

La conclusion est évidente en utilisant H0 et H, mais je ne sais pas comment utiliser H0 pour terminer la preuve . Merci beaucoup pour votre aide!

Answer 1

Depuis quelques temps et l'OP n'a pas répondu au commentaire de gallais, je vais mettre ici une solution qui devrait être facile à suivre en parcourant la preuve dans un IDE.

Require Import List. 

Lemma nth_eq : forall {A} (l1 l2 : list A), 
length l1 = length l2 -> 
(forall d k, nth k l1 d = nth k l2 d) ->l1 = l2. 
Proof. 
(* shortcut to the below: 
    induction l1; destruct l2; try discriminate 1. 
    will eliminate two of the cases for you *) 
induction l1; destruct l2. 
+ reflexivity. 
+ discriminate 1. 
+ discriminate 1. 
+ intros. f_equal. 
    - specialize H0 with (d := a) (k := 0). simpl in H0. assumption. 
    - apply IHl1. 
    * simpl in H. injection H. trivial. 
    * intros. specialize H0 with (d := d) (k := S k). simpl in H0. 
     assumption. 
Qed.