chdoc

Require Import Setoid Morphisms.
From mathcomp Require Import all_ssreflect.

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

Lemma iter_id (T : Type) n : @iter T n id =1 id.
Proof. by elim: n. Qed.