Lemma preZFS_Branch_isWellFounded (T : preZFS) (x : T) : Tree_isWellFounded (preZFS_Branch T x). Proof. unfold Tree_isWellFounded. split. - unfold isWellFoundedUp. intros S. set (SS := preZFS_Branch_hsubtype_tohsubtype T x S). intros X. assert (wfunder : Tree_isWellFounded (pr1 T)). { apply (pr12 T). } unfold Tree_isWellFounded in wfunder. unfold isWellFoundedUp in wfunder. unfold hasSmallest in wfunder. apply pr1 in wfunder. simpl in wfunder. set (L1 := wfunder SS). assert (L2 : (∃ x : pr11 (preZFS_Branch T x), S x) → ishinh_UU (∑ y : pr111 T, SS y)). { intros P. simpl in P. apply (P (ishinh (∑ y : pr111 T, SS y))). intros X1. destruct X1 as [te s]. destruct te as [t e]. simpl. unfold ishinh_UU. intros Q X1. apply X1. exists t. apply (fromBranch_hsubtype s). } apply L2 in X. apply L1 in X. apply (X (∃ x0 : pr11 (preZFS_Branch T x), S x0 ∧ (∀ y : pr11 (preZFS_Branch T x), S y ⇒ pr121 (preZFS_Branch T x) x0 y))). intros Y. destruct Y as [t [s π]]. assert (e : Ed T x t). { unfold SS in s. unfold preZFS_Branch_hsubtype_tohsubtype in s. apply (s (Ed T x t)). intros Y. destruct Y as [τ ξ]. apply τ. } assert (L4 : S (t ,, e)). { rewrite <- (Branch_to_subtype T x S). apply (toBranch_hsubtype e s). } simpl. unfold ishinh_UU. intros P Y. apply Y. exists (t ,, e). split. -- apply L4. -- intros xx Q. unfold Upw_E. simpl. apply π. unfold SS. simpl. unfold ishinh_UU. intros R Z. apply Z. exists (pr2 xx). apply Q. - unfold isWellFoundedDown. intros S. set (SS := preZFS_Branch_hsubtype_tohsubtype T x S). intros X. set (wfunder := pr212 T). unfold isWellFoundedDown in wfunder. unfold hasLargest in wfunder. simpl in wfunder. set (L1 := wfunder SS). assert (L2 : (∃ x : pr11 (preZFS_Branch T x), S x) → ishinh_UU (∑ y : pr111 T, SS y)). { intros Y. simpl in Y. apply (Y (ishinh (∑ y : pr111 T, SS y))). intros Z. destruct Z as [te s]. destruct te as [t e]. simpl. unfold ishinh_UU. intros P W. apply W. exists t. apply (fromBranch_hsubtype s). } apply L2 in X. apply L1 in X. apply (X (∃ xx : pr11 (preZFS_Branch T x), S xx ∧ (∀ y : pr11 (preZFS_Branch T x), S y ⇒ pr121 (preZFS_Branch T x) y xx))). intros Y. destruct Y as [t [s π]]. assert (e : Ed T x t). { unfold SS in s. unfold preZFS_Branch_hsubtype_tohsubtype in s. apply (s (Ed T x t)). intros Y. destruct Y as [τ ξ]. apply τ. } assert (L4 : S (t ,, e)). { rewrite <- (Branch_to_subtype T x S). apply (toBranch_hsubtype e s). } simpl. unfold ishinh_UU. intros P Y. apply Y. exists (t ,, e). split. -- apply L4. -- intros xx Q. unfold Upw_E. simpl. apply π. unfold SS. simpl. unfold ishinh_UU. intros R Z. apply Z. exists (pr2 xx). apply Q. Qed.