Definition step (T:Tree) {x z:T} (ne:x != z) : T := pr1 (mt_step _ x z ne).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.