proposition: Corollary chain_list_cons_inv x l y z : chain_list (x::l) y z -> x = y /\ exists k, R x k /\ chain_list l k z.
proof: Proof. intros H. apply chain_list_inv in H. destruct H as [ (? & _) | (k & l' & H & ? & ?) ]; try discriminate. inversion H; firstorder. Qed.
imports: Arith List Lia