Hi,

I’m stuck on proving something that seems very basic.

```
(* The type of binary relations *)
Definition Relation (A : Type) := A -> A -> Prop.
(* A relation terminates if it has no infinite chain *)
Definition terminates (A : Type) (R : Relation A) : Prop :=
~(exists u : nat -> A, forall k, R (u k) (u (S k))).
(* The "parallel product" of two relations *)
Definition parallel_product (A B : Type) (R : Relation A) (S : Relation B) : Relation (prod A B) :=
fun ab1 ab2 =>
let (a1, b1) := ab1 in
let (a2, b2) := ab2 in
R a1 a2 /\ S b1 b2.
(* If R or S terminates, the parallel product of R and S terminates.
Let's prove this with R. *)
Lemma parallel_product_terminates_if_one_argument_terminates
(A B : Type) (R : Relation A) (S : Relation B) :
terminates A R -> terminates (prod A B) (parallel_product A B R S).
Proof.
(* Let u an infinite chain for the parallel product of R and S. *)
intros H Ha. destruct Ha as [u Hu].
(* Extract an infinite chain for R. *)
apply H. exists (fun k => let (a, b) := u k in a).
(* Let's show this is indeed an infinite chain for R. *)
intro k. unfold parallel_product in Hu.
Fail apply Hu.
(* Unable to unify "let (a1, b1) := u ?M160 in let (a2, b2) := u (Datatypes.S ?M160) in R a1 a2 /\ S b1 b2"
with "R (let (a, _) := u k in a) (let (a, _) := u (Datatypes.S k) in a)". *)
destruct (u k) as [a b] eqn:Euk. destruct (u (Datatypes.S k)) as [a' b'] eqn:EuSk.
Fail rewrite Euk in Hu.
(* Found no subterm matching "u k" in Hu. *)
```

I can’t apply the hypothesis `Hu`

as-is, apparently because it’s not under the same form (`let`

s are outside the application of `R`

). I tried destructing `(u k)`

and `(u (Datatypes.S k))`

, but Coq doesn’t accept rewriting `Hu`

. Any hints on what I am doing wrong?