proposition: Theorem eq_dec : forall A (E F : gen_env A), (forall w w' : A, { w = w' } + { ¬ w = w' }) -> ok E -> ok F -> { E ≍ F } + { ¬ E ≍ F }.
proof: Proof. intros A E F Hdec Hok1 Hok2; unfold eq. elim all_binds_dec with A E F; elim all_binds_dec with A F E; intros; auto; right; intro Heq; destruct Heq; contradiction. Qed.
imports: Utf8 Equalities CoreGenericEnv