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