fill in proofs
WIP: was missing t1 ~ t2 |- <...,t1> --> <...,t2>
non-interference proof for updated calculus
non-interference at every step