proposition: Lemma dterm_subst1: forall {t': type} {E: context} {t: type} (a: term (t' :: E) t) (b: term E t') e, dterm (subst1 a b) e = dterm a (dterm b e, e).
proof: Proof. intros. unfold subst1. destruct (subst nil t' a b) as (c & C). apply C. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)