proposition: Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
proof: Proof. intros. rewrite <- nu_left_inv with (u := p1). rewrite <- nu_left_inv with (u := p2). now rewrite <- (nu_constant p1 p2). Qed.
imports: Arith