proposition: Lemma eq_rect_refl_eq : forall (A : Type) (p : A) (Q : A -> Type) (x : Q p) (h : p = p), eq_rect p Q x p h = x.
proof: Proof. Proof using. intros. rewrite~ (reflexive_identity_proofs_unique h). Qed.
imports: TLC(LibTactics LibAxioms)