proposition: Lemma env_subset_cons_none : forall E E', envSubset E' E -> envSubset (None :: E') (None :: E).
proof: Proof. intros; intros p A. destruct p; fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)