Library Substitution

Require Import InductiveFiniteSets.
Require Export JMeq.


Set Implicit Arguments.

Section Subs.


 Definition eq_subs :=
    fun (A : Type) (P : A -> Type) (a b : A)
         (H : a = b) (Pa : P a) => eq_rect a P Pa b H.

Definition dp_rwt : forall (A : Type) (B : A -> Type) (a a1 : A)
                       (P: forall a: A, forall x: B a, Type ) (b : B a)
                       (b1: B a1), a = a1 -> JMeq b b1 -> P a b -> P a1 b1 .
 Proof.
  intros A B a a1 P b b1 H; destruct H.
  intro jm; elim jm; trivial.
 Qed.

Definition dp_rwt1 : forall (A X: Set) (B : X -> Set) (F G : A -> X) (a a1 : A)
               (P: forall (a: A) (f : A -> X) , B (f a) -> Type ) (b : B (F a))
               (b1 : B (G a1)), a = a1 -> F = G -> JMeq b b1 -> P a F b ->
            P a1 G b1 .
Proof.
  intros A X B F G a a1 P b b1 H; destruct H.
  intro H1; destruct H1.
  intro jm; elim jm; trivial.
Qed.

 Lemma fs_eq : forall n : nat, forall x y : Fin n, x = y -> fs x = fs y .
 Proof.
  intros n x y H;
  apply (eq_subs (fun z => fs z = fs y) (sym_equal H));
  trivial.
 Defined .

Lemma fin_fs (n m : nat) (H : n = m) (i : Fin m) (J : Fin n) : JMeq i J -> JMeq (fs i) (fs J).
Proof.
  intros n m H i J H0 .
  apply (dp_rwt Fin (fun (x : nat) (fx : Fin x) => JMeq (fs fx) (fs J) ) H (sym_JMeq H0));
  trivial.
Defined.

End Subs.

Section SigT.

 Lemma sig_prj1 : forall (A : Type) (P : A -> Type)
   (x y : sigT P), projT1 x = projT1 y /\ JMeq (projT2 x) (projT2 y) -> x = y.
  Proof.
   destruct x; destruct y; simpl; auto.
   intro h; destruct h.
   cut (forall (A : Type) (B : A -> Type) (a a1 : A)
         (P : forall a0 : A, B a0 -> Type) (b : B a)
         (b1 : B a1), a = a1 -> JMeq b b1 -> P a b -> P a1 b1).
   intro H1.
   exact (H1 _ P _ _
          (fun a0 => fun (i : P a0) => existT P a0 i = existT P x0 p0 )
          _ _ (sym_equal H) (sym_JMeq H0)
         (refl_equal ( existT P x0 p0)) ). clear.
   intros A B a a1 P b b1 H; destruct H.
   intro H; case (JMeq_eq H); trivial.
 Qed.

 Definition sig_prj : forall (A : Type) (P : A -> Type)
   (x y : sigT P), x = y -> projT1 x = projT1 y /\ JMeq (projT2 x) (projT2 y).
   destruct x; destruct y.
   intro h; dependent rewrite h; auto.
 Defined.

End SigT.