proposition: Lemma choose_go_proper {i} (acc1 acc2 : Acc (choose_step _) i) : choose_go P1 acc1 = choose_go P2 acc2.
proof: Proof. Proof using Heq. induction acc1 as [i a1 IH] using Acc_dep_ind; destruct acc2 as [acc2]; simpl. destruct (Some_dec _) as [[x Hx]|]; [|done]. do 2 case_decide; done || exfalso; naive_solver. Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)