Definition iscontr_rect_compute' X (i : iscontr X) (x : X) (P : X ->UU) (p : P x) : iscontr_rect' X i x P p x = p. Proof. intros. unfold iscontr_rect'. induction (pr1 (isasetifcontr i x x (idpath _) (pr1 (isapropifcontr i x x)))). reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.