Dependently typed Data.Dynamic

Require Import Eqdep_dec_defined.

Section Cast.
  
  Variable U:Type.
  Variable F : U -> Type.
  
  Variable eq_dec : forall x y:U, {x = y} + {x <> y}.
  
  Definition eq_decide : forall x y:U, x = y \/ x <> y.
  intros x y; destruct (eq_dec x y); [ left | right ]; assumption.
  Defined.
  
  Definition cast (i j : U) : F j -> option (F i) :=
    fun J =>
      match eq_dec j i with
        | left Eql => match Eql in _ = i return option (F i) with
                        | refl_equal => Some J
                      end
        | right _ => None
      end.
  
  Theorem cast_reflexivity (i : U) (I : F i) : cast i i I = Some I.
    unfold cast; intro i; destruct (eq_dec i i);
      [ subst | absurd (i = i); tauto ].
    rewrite (eq_proofs_unicity eq_decide e (refl_equal i)).
    reflexivity.
  Defined.
  
  Definition cast_injective (i : U) (I I' : F i) :
    cast i i I = cast i i I' -> I = I'.
  intros i I I'; repeat rewrite cast_reflexivity.
  intro SomeEq; injection SomeEq; tauto.
  Defined.
  
  Inductive INeq (i : U)(I : F i) : forall (j : U)(J : F j), Prop :=
  | INeq_refl : INeq i I i I.
  Implicit Arguments INeq [i j].
  
  Hint Resolve INeq_refl.
  
  Definition INeq_eq (i : U)(I I' : F i) : INeq I I' -> I = I'.
  intros i I I' inEq; apply cast_injective.
  change ((fun i' I' => cast i i I = cast i i' I') i I').
  elim inEq; reflexivity.
  Defined.
  Implicit Arguments INeq_eq [i I I'].
  
  Lemma INeq_ind_r :
    forall (i:U) (I J:F i) (P:F i -> Prop), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rec_r :
    forall (i:U) (I J:F i) (P:F i -> Set), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rect_r :
    forall (i:U) (I J:F i) (P:F i -> Type), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Definition INeq_dec_dec :
    (forall (i:U)(I:F i) (j:U)(J:F j), {INeq I J} + {~INeq I J}) ->
    (forall (i:U)(I J:F i), {I = J} + {I <> J}).
  intros ineq_dec i I J; destruct (ineq_dec i I i J); [ left | right ].
  apply INeq_eq; assumption.
  contradict n; subst; reflexivity.
  Defined.
  
End Cast.