The Coq mailing list

[Éric Tanter <etanter AT dcc.uchile.cl>]

Hi Club,

Is there an automatic way to clean up the context of implications with 
obvious hypotheses?

For instance, I'd like to clean this up:

n : nat
H1: n = n -> fact1
H2: n = n -> fact2
========

as follows:

n : nat
H1: fact1
H2: fact2
========

in order to avoid to explicitly discharge n = n with reflexivity each time I 
use H1 and H2.

Thanks,

-- Éric