proposition: Theorem K_dec_point : forall P:x = x -> Type, P refl_equal -> forall p:x = x, P p.
proof: Proof. intros. elim eq_proofs_unicity_point with x refl_equal p. trivial. Defined.
imports: Equations.Init Equations.Prop.Classes