proposition: Theorem equiv_induction' (P : forall U V, U <~> V -> Type) : (forall T, P T T (equiv_idmap T)) -> (forall U V (w : U <~> V), P U V w).
proof: Proof. intros H0 U V w. apply (equiv_ind (equiv_path U V)). intro p; induction p; apply H0. Defined.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod