proposition: Lemma streicher_K : forall (A : Type) (x : A) (P : x = x -> Prop), P (refl_equal x) -> forall (p : x = x), P p.
proof: Proof. Proof using. intros. rewrite~ (reflexive_identity_proofs_unique p). Qed.
imports: TLC(LibTactics LibAxioms)