• Sylvain Dailler's avatar
    Add experimental coq realization for Fset and other Set theory · c5d97975
    Sylvain Dailler authored
    The underlying datastructure is not satisfying nor are the proofs but at
    least there is a quick simple realization. It uses ClassicalEpsilon axioms
    such as excluded middle, indefinite_description etc...
    Some theory realizations are very far from reality because the axiom
    characterization is small.
SetApp.v 1007 Bytes