proposition: Theorem all_binds_singles_eq_inv : forall A xs (vs vs' : list A) (F : gen_env A), List.NoDup xs -> length xs = length vs -> length xs = length vs' -> xs ∷ vs ⊏ F -> xs ∷ vs' ⊏ F -> vs = vs'.
proof: Proof. induction xs as [ | x xs IHxs ]; induction vs as [ | v vs IHvs ]; induction vs' as [ | v' vs' IHvs' ]; intros F Hnodup Hleq1 Hleq2 Habind1 Habind2; simpl in *; try congruence. inversion Hnodup. assert (((xs ∷ vs) & (x ∶ v)) ⊏ F) as Habind_1 by (rewrite <- singles_cons; auto); clear Habind1. assert (((xs ∷ vs') & (x ∶ v')) ⊏ F) as Habind_2 by (rewrite <- singles_cons; auto); clear Habind2. apply all_binds_l_concat_inv in Habind_1. apply all_binds_l_concat_inv in Habind_2. destruct Habind_1; destruct Habind_2. assert (vs = vs') as Heq1 by (apply IHxs with F; auto). assert (v = v') as Heq2 by (apply all_binds_single_eq_inv with x F; auto). rewrite Heq1, Heq2; auto. apply ok_concat. apply ok_singles; auto. apply ok_single. rewrite dom_singles. apply all_notin_single; auto. auto. rewrite dom_single. apply notin_all_notin. split. apply notin_singles; auto. apply all_notin_empty_l. apply ok_concat. apply ok_singles; auto. apply ok_single. rewrite dom_singles. apply all_notin_single; auto. auto. rewrite dom_single. apply notin_all_notin. split. apply notin_singles; auto. apply all_notin_empty_l. Qed.
imports: Utf8 Equalities CoreGenericEnv