environ given Fred being PERSON; given Hello being STATEMENT; KnightSpeak: for y being PERSON holds for s being STATEMENT holds Knight[y] & Tells[y,s] implies True[s]; begin == Specialize the y to Fred. 1: for s being STATEMENT holds Knight[Fred] & Tells[Fred,s] implies True[s] by KnightSpeak; == UE == Further Specialize the s in 1 to Hello. 2: Knight[Fred] & Tells[Fred,Hello] implies True[Hello] by 1; == UE == You must instantiate in the order that the quantifiers occur == thus attempting to specify s to Hello will not work. 3: for y being PERSON holds Knight[y] & Tells[y,Hello] implies True[Hello] by KnightSpeak; == That is, when you have a list of universal quantifiers, only the == leading ones can be eliminated. == In order to achieve the inner universal quantifier elimination you == have to use Universal Introduction, see below.