proposition: Lemma deClos_correct l s t : validComp s -> s >[(l)] t -> deClos s >(l) deClos t.
proof: Proof. Proof with repeat (cbn in * || eauto 10 using star || congruence || lia || subst). intros cs R. induction R... - eapply pow_trans;eauto. - inv cs;apply pow_step_congL... - inv cs;apply pow_step_congR... - rewrite Nat.sub_0_r. rewrite <-map_nth with (f:=deClos)... - inv H. inv cs. inv H1. eexists;split... rewrite <- subst_substList... Qed.