%% Arbitrary cascading substitutions on untyped lambda terms
%%
%% Nabla in the head of the definition of subst allows us to actively
%% manipulate the context of a term in order to make an arbitrary
%% number of substitutions for the nominal constants in the term.
%% Here we prove that this form of substitution acts compositionally.

Define subst nil T T.
Define nabla x, subst (pair x K :: L) (T x) S := subst L (T K) S.

Theorem subst_app : forall L T R S,
  subst L (app T R) S -> exists U V, S = app U V /\ subst L T U /\ subst L R V.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

Theorem subst_abs : forall L T R,
  subst L (abs T) R -> exists S, R = abs S /\ nabla z, subst L (T z) (S z).
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.