proposition: Lemma isaprop_folds_ax_id C : isaprop (folds_ax_I C).
proof: Proof. repeat (apply isapropdirprod). - apply impred; intro; apply isapropishinh. - repeat (apply impred; intro). apply pr2. - repeat (apply impred; intro). apply pr2. Qed.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets