PrP_tail_recursion a PrP project focused on implementing and verifying tail recursions Subtask 1 Add mutable reference to the original STLC and design the optimizing function under some restrictions. 夏潇恒 Prove Church–Rosser theorem under close term STLC.