Fail Check forall T n (t : n.-tuple T),
      let LHS := [LHS of size_tuple _] in
      let RDX := size (rev t) in
      [unify LHS with RDX].

The command has indeed failed with message:
In environment
T : Type
n : nat_eqType
t : n .-tuple T
LHS := (fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])(*...*) :
nat
RDX := size (rev t) : nat
The term "erefl LHS" has type "LHS = LHS"
while it is expected to have type "LHS = RDX" (cannot satisfy
constraint
"(fix size (s : seq ?T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end) ?t" == "(fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])").

Error:
In environment
T : Type
n : nat
t : n .-tuple T
LHS := size (tval ?94 ?92 ?96) (*...*) : nat
RDX := size (rev (tval n T t))           : nat
The term "erefl ?95" has type "?95 = ?95" while
it is expected to have type "LHS = RDX".