Skip to content

refactor(LocallyNameless): simplify proof of FullBeta.step_lc_r - #740

Merged
chenson2018 merged 2 commits into
leanprover:mainfrom
awesome-lambda-calculus:FullBeta.step_lc_r
Jul 25, 2026
Merged

refactor(LocallyNameless): simplify proof of FullBeta.step_lc_r#740
chenson2018 merged 2 commits into
leanprover:mainfrom
awesome-lambda-calculus:FullBeta.step_lc_r

inline proof

3cea411
Select commit
Loading
Failed to load commit list.

Select a check to view from the sidebar