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

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

Section FinFunDef.
  Variable (aT : finType). (* domain type *)
  Variable (rT : Type). (* codomain type *)

  Inductive finfun_type : Type := Finfun of #|aT|.-tuple rT. 
  Definition finfun_of of phant (aT -> rT) := finfun_type.
  Definition fgraph f := let: Finfun t := f in t.

  Canoni