fact: Definition x1_inj {z w : Pos} (p : x1 z = x1 w) : z = w := transport (fun s => z = ( match s with xH => w | x0 a => w | x1 a => a end)) p idpath.
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core