proposition: Lemma env_comp_sym : forall E1 E2, E1 [<->] E2 -> E2 [<->] E1.
proof: Proof. intros E1 E2 E1E2 x A B E2x E1x. sym; apply (E1E2 x); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)