Library Exercise_2_6_1_6


Require Import Utf8.
Require Import Isomorphism.

Set Implicit Arguments.

Section Exercise_2_6_1_6.
  Variable I : Type.
  Variable X : IType.

  Example Exercise_2_6_1_6 : Equivalence (λ i j, X i X j).
  Proof.
    split; hnf; simpl;
    eauto.
  Defined.
End Exercise_2_6_1_6.