proposition: Lemma env_eq_cons_inv_hd : forall a b E E', (a :: E) [=] (b :: E') -> a = b.
proof: Proof. intros. destruct a; destruct b; trivial. set (hint := (proj1 H) 0 s). fo; inversion H0; trivial. set (hint := (proj1 H) 0 s). fo; inversion H0; trivial. set (hint := (proj2 H) 0 s). fo; inversion H0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)