There is still no full implementation for inheriting constraints.
Subdirectories hoare and bledsoe of saturate/examples exercise ordering relations. In hoare you find lemmas that occur in the verification of quicksort and binary search algorithms. The directory bledsoe contains examples from various papers by Bledsoe, including the intermediate value theorem and the challenge problems stated in a JAR paper from 1990.