proposition: Lemma env_equiv_eq : forall E E', E [=] E' -> length E = length E' -> E = E'.
proof: Proof. induction E; destruct E'; intros; try_solve. rewrite (IHE E'). rewrite (env_eq_cons_inv_hd H); trivial. apply env_eq_cons_inv with a o; trivial. try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)