proposition: Theorem K_dec : forall P:x = x -> Type@{i}, P (id_refl x) -> forall p:x = x, P p.
proof: Proof. intros. elim eq_proofs_unicity with x (id_refl x) p. trivial. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes