Definition tree_induction (T:Tree) (x:T) (P:T->Type) (p0 : P x) (pn : ∏ z (ne:x != z), P (step T ne) -> P z) : ∏ z, P z. Proof. assert(d_ind : ∏ n z, mt_dist _ x z = n -> P z). { intro. induction n as [|n IH]. { intros. assert (k:x=z). { apply mt_anti. assumption. } destruct k. assumption. } { intros ? H. assert (ne : x != z). { intros s. exact (negpaths0sx _ (! mt_path_refl _ _ _ s @ H)). } refine (pn z ne _). { apply IH. unfold step; simpl. set (y := mt_step T x z ne). destruct y as [y [i j]]; simpl. apply invmaponpathsS. exact (i@H). } } } intro. apply (d_ind (mt_dist _ x z)). reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.