%% Correctness for LLambda subst predicate Specification "subst". Define ctx : olist -> olist -> prop by ctx nil nil ; ctx (term X :: L) (copy X X :: K) := ctx L K. Theorem ctx_member1 : forall L K E, ctx L K -> member E L -> exists T, E = term T /\ member (copy T T) K. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem ctx_member2 : forall L K E, ctx L K -> member E K -> exists T, E = copy T T. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem copy_id : forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. apply ctx_member1 to H1 H4. case H3. search. Theorem copy_eq : forall L K T S, ctx L K -> {K |- copy T S} -> T = S. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. apply ctx_member2 to H1 H4. case H3. search. Theorem subst : forall R T S, {term T} -> {subst R T S} -> R T = S. intros. case H2. apply copy_id to _ H1. inst H3 with n1 = T. cut H5 with H4. apply copy_eq to _ H6. search.