proposition: Lemma env_subset_cons_rev : forall a b E E', envSubset (a :: E') (b :: E) -> envSubset E' E.
proof: Proof. intros; intros p A D. set (w := H (S p) A D); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)