Added proofs for T_Atomic and T_InAtomic.