proposition: Lemma IsEither_dec: forall v a, {IsEither v a} + {~ IsEither v a}.
proof: Proof. intros. destruct a. destruct (equiv_dec v a). - left. red. left. simpl. assumption. - destruct (equiv_dec v a0). + left. red. right; simpl; assumption. + right. unfold IsEither. simpl. unfold equiv, complement in *. intuition. Defined.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver