see dependencies
import proveit %proving fold
fold may now be readily provable (assuming required theorems are usable). Simply execute "%qed".
%qed
proveit.logic.sets.enumeration.fold has been proven.