Lemma isatree_Upw (T : Tree) (x : pr11 T) : isatree (Upw_to_TRRGraph T x). Proof. unfold isatree. intros a. intros y z. simpl. set (zzz := ((pr1 (pr1 z)))). set (zz := (pr1 z)). set (yyy := ((pr1 (pr1 y)))). set (yy := (pr1 y)). assert (Eya : pr121 T yyy (pr1 a)). { unfold DownwardClosure in y. destruct y as [y σ]. simpl. apply σ. } assert (Eza : pr121 T zzz (pr1 a)). { unfold DownwardClosure in z. destruct z as [z σ]. simpl. apply σ. } split. - simpl. unfold antisymmetric. intros X. destruct X as [yz zy]. assert (L1 : zzz = yyy). { simpl in a. apply (pr1 (pr2 (T) (pr1 a) (yyy ,, Eya) (zzz ,, Eza)) (yz ,, zy)). } assert (p : pr1 zz = pr1 yy). { apply L1. } unfold Upw_to_TRRGraph in zz. unfold Upw_to_TRRGraph in yy. simpl in zz. simpl in yy. assert (q : pr2 zz = transportb (λ w, pr121 T x w) p (pr2 yy)). { apply proofirrelevance. apply (pr2 (pr121 T x (pr1 zz))). } apply (total2_paths_b p q). - assert (L : pr121 T yyy zzz ∨ pr121 T zzz yyy). { apply (pr2 ((pr2 (T)) (pr1 a) (yyy ,, Eya) (zzz ,, Eza))). } apply L. Qed.