(* TODO concrete definition by means of proof irrelevance *)
axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
(* TODO concrete definition by means of proof irrelevance *)
axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.