goal inclusion matching from jason

gistfile1.txt

Definition tmp {T} (x : T) := x.

Ltac first_goal_occurs_in_other_goal :=
  unshelve (
      repeat (let y := multimatch goal with
                       | [ |- context[?y] ] => y
                       | [ H : context[?y] |- _ ] => y
                       | [ H := context[?y] |- _ ] => y
                       end in
              is_evar y;
              lazymatch goal with
              | [ H : tmp (y = y) |- _ ] => fail
              | _ => pose proof (eq_refl y : tmp (y = y))
              end);
      [ > | shelve_unifiable.. ];
      let n1 := numgoals in
      shelve_unifiable;
      let n2 := numgoals in
      guard n2 < n1;
      (* cleanup now *)
      repeat match goal with
             | [ H : tmp (_ = _) |- _ ] => clear H
             end
    ).

Goal True.
  unshelve epose (_:nat) as n.
  all: first_goal_occurs_in_other_goal.
  2: clear.
  all: first_goal_occurs_in_other_goal. (* Error: Condition not satisfied: 2<2 *)