Hi there,

Consider a binary relation over a type and its reflexive transitive closure:

`Definition Rel (A:Type) := A -> A -> Prop.`

```
Inductive refltrans {A:Type} (R: Rel A) : Rel A :=
| refl: forall a, (refltrans R) a a
| rtrans: forall a b c, R a b -> refltrans R b c -> refltrans R a c.
```

The corresponding induction principle is given as follows:

```
forall (A : Type) (R : Rel A) (P : A -> A -> Prop),
(forall a : A, P a a) ->
(forall a b c : A, R a b -> refltrans R b c -> P b c -> P a c) -> forall y y0 : A, refltrans R y y0 -> P y y0
```

I want to prove a theorem whose environment at some point (after unfolding some definitions and generalizing some variables) seems to match the goal of the induction principle above:

```
A : Type
R : Rel A
HZ_prop : exists f : A -> A, forall a b : A, R a b -> refltrans R b (f a) /\ refltrans R (f a) (f b)
============================
forall a b : A, refltrans R a b -> forall c : A, refltrans R a c -> exists d : A, refltrans R b d /\ refltrans R c d
```

At this point I wanted to “`apply refltrans_ind`

” because I was expecting P to match with “`forall c : A, refltrans R a c -> exists d : A, refltrans R b d /\ refltrans R c d`

” but I get an error:

```
Error:
In environment
A : Type
R : Rel A
HZ_prop : exists f : A -> A, forall a b : A, R a b -> refltrans R b (f a) /\ refltrans R (f a) (f b)
Unable to unify "forall a : ?M160, ?M162 a a" with "A".
```

I managed to prove this theorem using the induction tactic directly, but I wanted to understand better the relation between the induction tactic and the use of the induction principle automatic generated by Coq for inductive definitions in more elaborated examples as the one above.

Any help is very much appreciated.

Regards,

Flávio.