Merge pull request #2119 from Alizter/ps/rr/rename_istrunc_inhabited_…

…istrunc

rename istrunc_inhabited_istrunc

theories/Basics/Trunc.v

@@ -536,12 +536,9 @@ Proof.
 Defined.
 
 (** If a type [A] implies that it is [n.+1]-truncated, then it is [n.+1]-truncated. **)
-Definition istrunc_self_implies_istrunc {n : trunc_index} {A : Type} (H : A -> IsTrunc n.+1 A)
-  : IsTrunc n.+1 A.
-Proof.
-  apply istrunc_S.
-  intros a b.
-  exact (H a a b).
-Defined.
+Definition istrunc_inhabited_istrunc {n : trunc_index}
+  {A : Type} (H : A -> IsTrunc n.+1 A)
+  : IsTrunc n.+1 A
+  := istrunc_S _ (fun a b => H a a b).
 
 (** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)