(** %
\section{\label{sec:util}Util}
% *)
Module Export util.

Require Import Equality.
Require Import List.

Ltac solveFirstIn hyp
    := let v := fresh "SFI" in
       match type of hyp with
       | ?t -> _ => assert (v : t); [ idtac | specialize (hyp v); try (clear v) ]
       end.

Ltac solveExists :=
    match goal with
    | |- ex (fun _ : ?y => _) =>
        let seVar := fresh "seVar"
        in assert (seVar : y); [ | exists seVar ]
    | |- sig (fun _ : ?y => _) =>
        let seVar := fresh "seVar"
        in assert (seVar : y); [ | exists seVar ]
    | |- sigT (fun _ : ?y => _) =>
        let seVar := fresh "seVar"
        in assert (seVar : y); [ | exists seVar ]
    end.

Ltac proofIrrel H1 H2 :=
    let Heq := fresh "Heq" in
    assert (Heq : H1 = H2); [apply proof_irrelevance | subst].

Program Fixpoint inmap
    {A B : Type}
    (l : list A)
    (f : forall x : A, In x l -> B)
  : list B
 := match l with
    | nil => nil
    | cons x xs => f x _ :: inmap xs _
    end.
Next Obligation.
auto with *.
Qed.
Next Obligation.
specialize (f x).
auto with *.
Qed.

Lemma map_neq_nil : forall {t1 t2 : Type}
                           {l : list t1}
                           {f : t1 -> t2},
                    l <> nil
                 -> map f l <> nil.
Proof with auto.
intros.
intro.
apply map_eq_nil in H0.
congruence.
Qed.

Lemma map_neq_nil2 : forall {t1 t2 : Type}
                           {l : list t1}
                           {f : t1 -> t2},
                    map f l <> nil
                 -> l <> nil.
Proof with auto.
intros.
intro.
elim H.
subst.
unfold map...
Qed.

End util.