open main
pred idQS6cySANCTJXecpK9_prop19 {
	all f : Protected | f in Protected until f in Trash
}
pred __repair { idQS6cySANCTJXecpK9_prop19 }
check __repair { idQS6cySANCTJXecpK9_prop19 <=> prop19o }