Theorem Equiv_rect (X Y : Struc) (P : X ≅ Y -> UU) : (∏ e : X = Y, P (Struc_univalence _ _ e)) -> ∏ f, P f. Proof. intros ih f. set (p := ih (invmap (Struc_univalence _ _) f)). set (h := homotweqinvweq (Struc_univalence _ _) f). exact (transportf P h p). Defined.