Verification of the congruence closure algorithm in Coq using dependent types.
Main Files with final proofs: transitive_closure_rewrite.v, congruence_closure_rewrite_suffix.v (With changed type for merge)
Other files contain different proof strategies in various stages on completion. Some of which are doomed. :)