for f being INT-Exec
for v being INT-Variable of NAT
for t being INT-Expression of NAT holds v,t form_assignment_wrt f