proposition: Theorem equiv_induction_inv {U : Type} (P : forall V, V <~> U -> Type) : (P U (equiv_idmap U)) -> (forall V (w : V <~> U), P V w).
proof: Proof. intros H0 V. apply (equiv_ind (equiv_path V U)). revert V; rapply paths_ind_r; apply H0. Defined.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod