proposition: Lemma validComp_step s t l: validComp s -> s >[(l)] t -> validComp t.
proof: Proof. Proof with repeat (subst || firstorder). intros vs R. induction R;repeat inv_validComp... - inv H3. constructor... - inv H3. apply H1. apply nth_In. lia. - inv H8. constructor;auto;intros a [?|?];subst;auto. Qed.