added Isabelle variant with varying domain quantification for individuals