proposition: Lemma f_sos_sos_step : forall r i r' i', f_sos r i = Some(r',i') -> sos_step r i i' r'.
proof: Proof. Proof with eauto. intros r i r'; induction i; intros i' H. simpl in H; unbind_hyp H v1 He; unbind_hyp H r1 Hu; injection H; intros; subst... simpl in H. destruct (eq_skip i1). subst i1; injection H; intros; subst... unbind_hyp H p H1; destruct p; injection H; intros; subst... simpl in H; unbind_hyp H t Ht; destruct t; injection H; intros; subst... simpl in H; discriminate. Qed.
imports: ZArith List syntax Lia