fact: Fixpoint proj_env (E': context) (E: context) : dcontext (E' ++ E) -> dcontext E := match E' with | nil => fun e => e | t :: E' => fun e => proj_env E' E (snd e) end.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)