Congruence Closure Procedure in Cubical Agda

Automate proofs constructed using properties of equality; reflexivity, symmetry, transivity and congruence.

An extension of Selsam and de Moura's procedure in Intensional Type Theory to support Cubical Type Theory.

Installing

TBA

Usage

For now just look at the file src/Examples.agda