No title

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Ltac instantiate_pair :=
  match goal with
  | |- context[ @fst ?A ?B ?x ] => is_evar x;
        let x1 := fresh in let x2 := fresh in
        evar (x1 : A); evar (x2 : B);
        unify x (@pair A B x1 x2); clear x1 x2
  end.
Ltac instantiate_pairs :=
  repeat (instantiate_pair; simpl fst; simpl snd).

Goal exists x : nat * nat, fst x = 1 /\ snd x = 2.
  eexists; instantiate_pairs; intuition.
Qed.

Goal exists x : (nat * nat * nat), fst (fst x) = 1 /\ snd (fst x) = 2 /\ snd x = 3.
  eexists; instantiate_pairs; intuition.
Qed.