for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V ex f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai