proposition: Lemma boxed_option_nil {A} : forall (P: A -> Prop), forall x, boxed_option (fun x : A => P x) x ↝ [] -> (~ P (indexedElement x)).
proof: Proof. unfold boxed_option; simpl; intros. apply Pick_inv in H; intuition. computes_to_inv; intuition; discriminate. Qed.
imports: Coq.Lists.List Coq.Program.Program Coq.Sets.Ensembles Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation