proposition: Lemma isEmptyTwoCases: forall l, isEmpty l = Vone \/ isEmpty l = Vzero.
proof: Proof. intros. induction l. 1: simpl; left; trivial. destruct IHl; simpl; destruct (Z_lt_dec a (inf+1)); (try now left); now right. Qed.
imports: VST.floyd.proofauto