proposition: Lemma env_comp_cons : forall e1 e2 E1 E2, E1 [<->] E2 -> (e1 = e2 \/ e1 = None \/ e2 = None) -> (e1::E1) [<->] (e2::E2).
proof: Proof. unfold env_comp. intros e1 e2 E1 E2 E_comp e1e2 x A B E1_x E2_x. destruct e1e2 as [e1e2 | [e1e2 | e1e2]]; first [rewrite e1e2 in E1_x | rewrite e1e2 in E2_x]; destruct x; unfold VarD in *; simpl in *; solve [congruence | discr | apply E_comp with x; trivial]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)