Lemma isdecinclpr1 {X : UU} (P : X -> UU) (is : ∏ x : X, isdecprop (P x)) : isdecincl (@pr1 _ P). Proof. intros. intro x. assert (w : weq (P x) (hfiber (@pr1 _ P) x)) by apply ezweqpr1. apply (isdecpropweqf w (is x)). Defined.