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.