proposition: Lemma appUnits_subst_c M G W i (MG: correct_subst M G) : nth_error (appUnits M) i = Some W -> correct_subst W G.
proof: Proof. intro. destruct MG. assert (isAppUnit W M). unfold isAppUnit. apply nth_some_in with i; trivial. constructor; trivial. rewrite (appUnit_env W M H0); trivial. rewrite (appUnit_env W M H0); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)