proposition: Lemma dep_pair_eq : forall {T : Type} {a b : T} (eq : a = b) (P : T -> Prop) (pa : P a) (pb : P b), @eq_rect T a P pa b eq = pb -> exist P a pa = exist P b pb.
proof: Proof. intros. rewrite <- H. rewrite <- eq. reflexivity. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega