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