proposition: Lemma isEmpty_in: forall l target, In target l -> target < inf + 1 -> isEmpty l = Vzero.
proof: Proof. intros. 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. Qed.
imports: VST.floyd.proofauto