proposition: Lemma cbv_cbn_subst sigma s : (forall n, match sigma n with | app _ _ => False | _ => True end) -> cbv_cbn (subst sigma s) = subst (funcomp Psi sigma) (cbv_cbn s).
proof: Proof. elim: s sigma. - move=> n sigma Hsigma /=. have := Hsigma n. by case: (sigma n). - move=> s IH1 t IH2 sigma Hsigma /=. rewrite (IH1 _ Hsigma) (IH2 _ Hsigma) /=. rewrite !simpl_term /=. congr lam. congr app. congr lam. congr app. apply: ext_subst_term => ? /=. by rewrite !simpl_term. - move=> s IH sigma Hsigma /=. rewrite IH. { move=> [|n] /=; first done. have := Hsigma n. by case: (sigma n). } rewrite !simpl_term. congr lam. congr app. congr lam. apply: ext_subst_term => - [|n] /=; first done. have := Hsigma n. case: (sigma n); [done|done|]. move=> s' /= _. rewrite !cbv_cbn_ren. congr lam. rewrite !simpl_term. apply: ext_ren_term. by case. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)