proposition: Lemma nv2v_implication : forall nvl vl, (forall nv, exists v, In nv nvl -> nv = (normal_step_v v))-> nv2v nvl = vl -> length nvl = length vl.
proof: Proof. intros. inversion_clear H0. induction nvl. compute;reflexivity. destruct (H a). rewrite H0. simpl. apply f_equal. apply IHnvl. intros. destruct (H nv). exists x0. auto with datatypes. apply in_eq. Qed.
imports: Coq(List) Coq(Relation_Operators)