fact: Definition Trunc_ind {n A} (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} : (forall a, P (tr a)) -> (forall aa, P aa) := (fun f aa => match aa with tr a => fun _ => f a end Pt).
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality