proposition: Lemma rSubstList_correct phi s x A: Proc phi -> denoteTerm phi (rSubstList s x A) = substList (denoteTerm phi s) x (map (denoteTerm phi) A).
proof: Proof. revert x. induction s; intros;simpl. - decide (x < x0); decide (x0 > x); try lia ;intuition (try congruence);simpl. now rewrite <-map_nth with (f:= denoteTerm phi). - now rewrite IHs1,IHs2. - now rewrite IHs. - rewrite substList_closed. auto. apply H. - rewrite IHs. 2:tauto. reflexivity. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd