fact: Fixpoint Vsig_of_forall n (v : vector A n) : Vforall P v -> vector (sig P) n := match v in vector _ n return Vforall P v -> vector (sig P) n with | Vnil => fun _ => Vnil | Vcons a w => fun H => Vcons (exist (proj1 H)) (Vsig_of_forall w (proj2 H)) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)