michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

minor tweak

Browse source
This commit is contained in:
Jeremy Siek 2019-05-06 15:01:34 +02:00
parent 27983098b0
commit 4658c1e275
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
extra/extra/CallByName.lagda
View file

@ -122,8 +122,7 @@ commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r = cong ƛ_ IH
ρ' {∅} = λ ()
ρ' {Γ , ★} = ext ρ
H : {x : Γ , ★ ∋ ★} →
exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
H : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
H {Z} = refl
H {S x} =
begin