proposition: Theorem K {A} `{IsHSet A} (x : A) (P : x = x -> Type) : P 1%path -> forall p : x = x, P p.
proof: Proof. intros. exact (is_hset 1 p # X). Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Classes HoTT.Basics.Trunc