#4: forall&exist axiom fixed. #5: now available correct subst of var for term