Require Export LibDefaultSimp.

Inductive incV (V : Set) : Set :=
| VZ : incV V
| VS : V → incV V
.

Arguments VZ {V}.
Arguments VS {V} _.

Definition incV_map {V W : Set} (f : V → W) (x : incV V) : incV W :=
  match x with
  | VZ ⇒ VZ
  | VS y ⇒ VS (f y)
  end.

Ltac destruct_hyps :=
  repeat match goal with H: ?T |- _ ⇒
    match T with
    | _ ∧ _ ⇒ destruct H
    | ∃ a, _ ⇒ destruct H
    end
  end.