auto gitdoc commit

This commit is contained in:
Michael Zhang 2024-04-22 04:26:07 +00:00
parent 4e75616580
commit 7f02bfa071

View file

@ -421,7 +421,7 @@ theorem2∙13∙1 m n = encode m n , equiv
res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
res = {! !}
in {! !}
in res
equiv = record
{ g = decode m n