proposition: Theorem all_binds_dec_exists : forall A xs (F : gen_env A), List.NoDup xs -> { vs : list A | length xs = length vs ∧ (xs ∷ vs) ⊏ F } + { forall vs : list A, length xs = length vs -> ¬ (xs ∷ vs) ⊏ F }.
proof: Proof. intros A xs F Hnodup. unfold all_binds. induction xs as [ | x xs IHxs ]. Focus. left. exists nil. split; auto. rewrite singles_empty. intros x v Hbind. apply binds_empty in Hbind. inversion Hbind. assert (~ List.In x xs ∧ List.NoDup xs) as Hnodup2 by (inversion Hnodup; auto). clear Hnodup. destruct Hnodup2 as [ Hnotin Hnodup2 ]. destruct IHxs as [ IH | IH ]; auto. Focus. destruct IH as [ vs [ Hlen Hbind ] ]. elim binds_dec_exists with A x F; intro Hex. destruct Hex as [ v Hbind2 ]. left. exists (v :: vs). split; simpl; auto. intros y w Hbind3. assert (y ∹ w ⋲ ((xs ∷ vs) & (x ∶ v))) as Hbind4 by (rewrite <- singles_cons; auto). clear Hbind3. apply binds_concat_inv in Hbind4. destruct Hbind4 as [ Hbind4 | [ Hnotin2 Hbind4 ] ]; auto. apply binds_single_inv in Hbind4. destruct Hbind4; subst; auto. right. intros ws Hlen2. inversion Hlen2 as [ Hlen3 ]. apply eq_sym in Hlen3. apply list_length_S in Hlen3. destruct Hlen3 as [ w [ ws' Heq ] ]; subst; simpl in *. intro Hyp. apply (Hex w). apply (Hyp x w). assert (x ∹ w ⋲ ((xs ∷ ws') & (x ∶ w))). apply binds_concat_r. apply binds_single; auto. rewrite singles_cons; auto. Focus. right. intros vs Hlen. inversion Hlen as [ Hlen2 ]. apply eq_sym in Hlen2. apply list_length_S in Hlen2. destruct Hlen2 as [ v [ vs' Heq ] ]. subst; simpl in *. intro Hyp. apply (IH vs'); auto. intros y w Hbind. apply Hyp. assert (y ∹ w ⋲ ((xs ∷ vs') & (x ∶ v))); auto. apply binds_concat_l; auto. apply binds_belongs in Hbind. inversion Hlen. apply belongs_singles_inv in Hbind; auto. apply notin_single. intro Heq; subst; auto. rewrite singles_cons; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv