Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype seq tuple.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition trev T n (t : n.-tuple T) := [tuple of rev t].
Lemma trevK T n : involutive (@trev T n).
Proof. by move=>t; apply: val_inj; rewrite /= revK. Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment