rev (rev s) = s

revrevid.v

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma cons_rcons T (x1 x2 : T) s : x1 :: rcons s x2 = rcons (x1 :: s) x2.
Proof. done. Qed.

Theorem rev_rev_id T (s : seq T) : rev (rev s) = s.
Proof.
  elim: s => // x s. rewrite rev_cons. case: (rev s) => [|x1 s1] <- //=.
  rewrite cons_rcons rev_rcons => //=.
Qed.