{m n} (Hmn : m <= n) `{IsTrunc m A} : IsTrunc n A. Proof. generalize dependent A; generalize dependent m. simple_induction n n' IH; intros [ | m'] Hmn A ? . - assumption. - destruct Hmn. - apply @istrunc_succ, (IH (-2)); auto. - apply istrunc_S. intros x y; apply (IH m'); auto with typeclass_instances. Defined.
Require Import