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