Lemma isaprop_ZFS_elementof (X Y : ZFS) : isaprop (ZFS_elementof X Y). Proof. apply invproofirrelevance. unfold isProofIrrelevant. intros z w. unfold ZFS_elementof in z. unfold ZFS_elementof in w. destruct z as [z [ ispp p]]. destruct w as [w [ ispq q]]. set (r := (! q) @ p). apply total2_paths_equiv in r. destruct r as [r ρ]. set (s := (pr2 Y w z r)). simpl in ρ. set (τ y := @isapropdirprod _ _ (isaprop_isapoint y) (isaset_ZFS X (Y ↑ y))). set (P := λ y : Y, (isapoint y × X = Y ↑ y) ,, τ y). apply (total2_paths_hProp_equiv P (z,, (ispp,, p)) (w,, (ispq,, q))). simpl. apply (! s). Qed.