proof_using_type.v

Require Import Coq.Logic.EqdepFacts.

Set Implicit Arguments.

Inductive ext : Type :=
| ext_ : forall (X: Type), X -> ext.

Variable eqXY: forall X, X -> X -> Prop.

Inductive Eq_ext (X : Type) : ext -> ext -> Prop :=
| eq_ext : forall (x y: X),
    eqXY x y ->
    Eq_ext X (ext_ x) (ext_ y).

Variable eqXY_trans: forall X (x y z:X), eqXY x y -> eqXY y z -> eqXY x z.

Axiom eq_dep_eq : Eq_dep_eq Type.

Lemma ext_eq X (x y : X) : ext_ x = ext_ y -> x = y.
Proof.
  intros H.
  inversion H.
  apply eq_dep_eq__inj_pair2 in H1; auto.
  apply eq_dep_eq.
Qed.

Lemma Eq_trans :
  forall (X : Type) (x y z: ext),
    Eq_ext X x y -> Eq_ext X y z -> Eq_ext X x z.
Proof.
  intros X x y z Hxy Hyz.
  destruct Hxy as [x' y' x'y'].
  remember (ext_ y') as ey' eqn:Eq.
  destruct Hyz as [y'' z' y''z'].
  apply ext_eq in Eq; subst.
  constructor.
  now apply eqXY_trans with (y := y').
Qed.