fill in proofs
WIP: was missing t1 ~ t2 |- <...,t1> --> <...,t2>