# Reflexive and transitive closure

Define inductively the reflexive and transitive closure of a binary relation.

Prove that your solution is equivalent to the impredicative
definition of `Rstar` given in the module `Rstar` of the
standard library.
## Solution

Look at this file .

Going home

Pierre Castéran