(x : ((Cantor + Cantor) + Cantor) + Cantor) : I0 (ff_flip x) = f_flip (I0 x) := ap10_equiv (Inat (f (point (BAut Cantor))) (f (point (BAut Cantor))) (equiv_sum_symm Cantor Cantor)) x.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.