proposition: Theorem length_subst: forall n v l, length (subst n v l) = length l.
proof: Proof. intros n; elim n; simpl; auto. intros v l; case l; simpl; auto. intros n1 Rec v l; case l; simpl; auto. Qed.
imports: List ListAux UList OrderedList