proposition: Lemma env_comp_sub : forall E1 E2 E3, E1 [<->] E2 -> E1 [-] E3 [<->] E2.
proof: Proof. induction E1; auto. intros E2 E3 E12 p A B. destruct p; unfold VarD. destruct a; destruct E3; destruct E2; try destruct o; try destruct o0; solve [ try_solve | intros sA sB; inversion sA as [s_A]; rewrite <- s_A; inversion sB as [s_B]; rewrite <- s_B; apply (E12 0); unfold VarD; trivial ]. destruct a; destruct E3; destruct E2; try destruct o; try destruct o0; try solve [ try_solve | apply (E12 (S p) A B) | apply (IHE1 E2 E3 (env_comp_tail E12) p A B) ]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)