proposition: Lemma sos_step_imp_sn : forall r r' i i', sos_step r i i' r' -> forall r'', exec r' i' r'' -> exec r i r''.
proof: Proof. induction 1; intros r2 Hexec; try (inversion Hexec; subst; eauto). Qed.
imports: ZArith List syntax Lia