fact: Definition I0_preserves_inr (x : Cantor + Cantor + Cantor + Cantor) : (is_inr x + is_inl_and is_inr x) <-> is_inr (I0 x).
imports: HoTT.Basics HoTT.Types Idempotents HoTT.Truncations.Core Spaces.BAut Spaces.Cantor