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