proposition: Lemma Upw_transitive (T : Tree) (x : pr11 T) : ∏ y z w, (Upw_E T x) y z → (Upw_E T x) z w → (Upw_E T x) y w.
proof: Proof. intros y z w P Q. unfold Upw_E in P. simpl in P. exact (TRRG_transitivity (pr1 T) (pr1 y) (pr1 z) (pr1 w) P Q). Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions