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