proposition: Theorem eq_trans : forall A (E F G : gen_env A), E ≍ F -> F ≍ G -> E ≍ G.
proof: Proof. unfold eq; intros A E F G Heq1 Heq2. destruct Heq1, Heq2. split; apply all_binds_trans with F; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv