Definition iscontr_rect' X (i : iscontr X) (x0 : X) (P : X ->UU) (p0 : P x0) : ∏ x:X, P x. Proof. intros. induction (pr1 (isapropifcontr i x0 x)). exact p0. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.