{x : X & P x}. Proof. set (P' n := P (e n)). assert (P'_dec : forall n, Decidable (P' n)) by apply _. assert (P'_inhab : hexists (fun n => P' n)). { strip_truncations. apply tr. destruct P_inhab as [x p]. exists (e ^-1 x). unfold P'. rewrite (eisretr e). exact p. } destruct (minimal_n P' P'_dec P'_inhab) as [n p']. exists (e n). exact p'. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Truncations.Core. Require Import HoTT.Spaces.Nat.Core.