proposition: Theorem all_binds_dec : forall A (E F : gen_env A), ok E -> (forall w w' : A, { w = w' } + { ¬ w = w' }) -> {E ⊏ F} + {¬ E ⊏ F}.
proof: Proof. assert (forall A, (forall w w' : A, { w = w' } + { ¬ w = w' }) -> forall ws ws' : list A, { ws = ws' } + { ¬ ws = ws' }) as Hdec. intros A Hyp. induction ws as [ | w ws IHws ]; induction ws' as [ | w' ws' IHws' ]; simpl in *; auto. right; intro Heq; inversion Heq. right; intro Heq; inversion Heq. destruct (Hyp w w'); destruct (IHws ws'). left; subst; auto. right; intro Heq; inversion Heq; auto. right; intro Heq; inversion Heq; auto. right; intro Heq; inversion Heq; auto. intros A E F Hok Hdec2. assert (forall ws ws' : list A, { ws = ws' } + { ¬ ws = ws' }) as Hdec3 by auto. assert (List.NoDup (dom E)) as Hdom by (apply ok_dom_inv; auto). elim all_binds_dec_exists with A (dom E) F; auto; intro Hyp. destruct Hyp as [ vs [ Hlen Habind ] ]. elim (Hdec3 vs (img E)); intro Hyp; subst. left. rewrite dom_img_id in *; auto. right. intro Habind2. rewrite <- (dom_img_id E) in Habind2. assert (vs = img E). apply all_binds_singles_eq_inv with (dom E) F; auto. apply length_dom_img_eq. auto. right. intro Habind. apply (Hyp (img E)). apply length_dom_img_eq. rewrite dom_img_id; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv