HITs-Examples/FiniteSets/FSets.v

3 lines
131 B
Coq

Require Export HoTT HitTactics.
Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality prelude.