(x y z : No) : (x + y) + z = x + (y + z). Proof. one_line_proof (equiv_sum_assoc _ _ _) (equiv_sum_assoc _ _ _); one_line_proof 1%equiv 1%equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.