Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.

No title

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
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.

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