This git repo is for paper submission, review and evaluation. These files are
part of a Coq formalization project, CommonKnowledge, which will be open source
in the future.

For the countability part, most examples are in
    Relations/CountableExamples.v
and most proofs are in
    IndType/Syntax.v
    Relation/Countable.v
    Relation/SetoidCountable.v
    Relation/SetoidCountable.v
    Relation/IndCountable_AuxDefs.v
    Relation/IndCountable.v

A benchline proof based on old tactic-based proof scripts are in
    Relations/CountableExamplesComparison.v

This repo can be compiled under Coq 8.12. Command line "make depend" + "make"
will complete the compilation.

Developers: Qinxiang Cao, Xiwei Wu.