proposition: Lemma env_comp_subset : forall El Er El' Er', El [<->] Er -> envSubset El' El -> envSubset Er' Er -> El' [<->] Er'.
proof: Proof. fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)