fact: Fixpoint env_compose (E F: Env) : Env := match E, F with | nil, nil => EmptyEnv | L, nil => L | nil, L => L | _::E', Some a::F' => Some a :: env_compose E' F' | e1::E', None::F' => e1 :: env_compose E' F' end.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)