fact: Definition lift (E': context) (t': type) {E: context} {t: type} (a: term (E' ++ E) t) : { b : term (E' ++ t' :: E) t | forall e, dterm b e = dterm a (unlift_env E' t' E e) }.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)