proposition: Lemma isEmpty_in': forall l, (exists i, In i l /\ i < (inf + 1)) <-> isEmpty l = Vzero.
proof: Proof. split; intros. - destruct H as [? [? ?]]. induction l. 1: exfalso; apply (in_nil H). unfold isEmpty. rewrite fold_right_cons. destruct (Z_lt_dec a (inf+1)); trivial. simpl in H; simpl; destruct H. 1: rewrite H in n; exfalso; lia. clear n a. specialize (IHl H). unfold isEmpty in IHl. trivial. - induction l. 1: inversion H. simpl in H. destruct (Z_lt_dec a (inf+1)). + exists a. split; simpl; [left|]; trivial. + destruct (IHl H) as [? [? ?]]. exists x. split; [apply in_cons|]; assumption. Qed.
imports: VST.floyd.proofauto