an experiment with proving records with irr. fields equal
	modified:   Equality.agda