The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 09/30/2015 06:43 PM, Patricia Peratto wrote:
> I need to use congruence of equality.
> I import the files Logic and Logic_Type
> but does not find it. (I want to use the
> function congr_id).
>
> Is it in another place?
>
> Regards
> Patricia Peratto


This given by the inductive principle derived from the definition
of eq.

Print eq_ind.

This is what the rewrite tactic is using.

Goal forall (A : Type) (a b : A), a = b -> id a = id b.
intros A a b H.
rewrite H.
apply refl_equal.
Qed.


You can also have a look in Init/Logic.v at theorems such as f_equal, 
f_equal2....

Goal forall (A : Type) (a b : A), a = b -> id a = id b.
intros A a b H.
apply f_equal.
exact H.
Qed.

--
Laurent