id="code-wrapper">
      <div id="document">

<h1>Chapter 7_2</h1><div><textarea id='coq-code'>
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Chapter72.
  Definition tcmp n (T : eqType) (t1 t2 : n.-tuple T) := tval t1 == tval t2.

  Lemma eqtupleP n (T : eqType) : Equality.axiom (@tcmp n T).
  Proof.
    move => x y; apply: (iffP eqP); last first.
      by move => ->.
      case: x; case y => s1 p1 s2 p2 /= E.
      rewr