proposition: Theorem peq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
proof: Proof. intros. elim pnu_left_inv with (u := p1). elim pnu_left_inv with (u := p2). elim nu_constant with y p1 p2. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes