Theorem preZFS_univalence (X Y : preZFS) : (X = Y) ≃ (preZFS_iso X Y). Proof. set (P := λ x, λ y, Tree_univalence x y). set (Q := λ x, (ispreZFS x ,, isaprop_ispreZFS x)). exact (substructure_univalence _ _ P Q X Y). Qed.