proposition: Lemma env_comp_tail : forall e1 e2 E1 E2, (e1::E1) [<->] (e2::E2) -> E1 [<->] E2.
proof: Proof. unfold env_comp. intros e1 e2 E1 E2 E_comp x A B E1_x E2_x. apply (E_comp (S x) A B); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)