proposition: Lemma env_subset_trans : forall E1 E2 E3, envSubset E1 E2 -> envSubset E2 E3 -> envSubset E1 E3.
proof: Proof. fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)