proposition: Lemma f_star_sem : forall n r i r' i', f_star n r i = Some(r',i')-> sos_star r i i' r'.
proof: Proof. Proof with eauto. induction n; intros r i r' i' H. simpl in H; injection H; intros; subst; eauto. simpl in H. destruct (eq_skip i). subst i; injection H; intros; subst... unbind_hyp H p H1; destruct p as [r1 i1]... Qed.
imports: ZArith List syntax Lia