proposition: Lemma env_eq_cons_inv : forall a b E E', (a :: E) [=] (b :: E') -> E [=] E'.
proof: Proof. intros. change E with (tail (a :: E)). change E' with (tail (b :: E')). apply env_eq_tail; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)