proposition: Theorem K {A} `{HSet A} (x : A) (P : x = x -> Type) : P (id_refl x) -> forall p : x = x, P p.
proof: Proof. intros. exact (transport (is_hset id_refl p) X). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes