proposition: Theorem pos_S_invert n P : P (@pos_fst n) -> (forall p, P (pos_nxt p)) -> forall p, P p.
proof: Proof. intros; apply pos_invert; split; auto. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)