The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I think the following does what you want:

Goal forall (n m : nat) (n' m' : unit) (f : nat -> nat -> Type) (f' :
unit -> unit -> Type) (P : nat -> Prop) (fn : P n -> f n m -> f' n'
m'), False.
     intros.
match goal with
  | [ H : unit -> unit -> _, H1 : appcontext[?H' ?a ?b] |- _ ] =>
constr_eq H H'; pose H
end.

Cheers
Thomas


On Thu, Aug 9, 2012 at 3:48 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Goal forall (n m : nat) (n' m' : unit) (f : nat -> nat -> Type) (f' : unit
> -> unit -> Type) (P : nat -> Prop) (fn : P n -> f n m -> f' n' m'), False.
>       intros.
>       match goal with
>         | [ H : unit -> unit -> _, H1 : appcontext[?H ?a ?b] |- _ ] => pose
> H
>       end.