Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 23:00:30 -05:00
21d9a2ce1b Add standardization_lo
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 22:44:05 -05:00
bdba6f50e5 Finish the soundness proof completely
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 20:43:19 -05:00
d24991e994 Finish most of the neu abs case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 20:42:54 -05:00
b38a422551 Finish most of the pair case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 19:51:31 -05:00
49a254fbef Finish the pair pair case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 19:15:05 -05:00
60a4eb886f Finish injectivity for pairs
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 01:22:38 -05:00
06d420aa7e Add stubs for lemmas needed for completeness
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 01:13:49 -05:00
0f48a485be Prove some impossible cases
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-15 17:22:55 -05:00
3fb6d411e7 Finish most of the pi pi case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-15 16:39:11 -05:00
926c2284a5 Finish the pair pair case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-15 14:31:43 -05:00
9d951a24c5 Add standardization theorem for djoin
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-15 14:05:11 -05:00
67f91970d6 Finish the admitted inversion lemmas that depend on SN
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 21:55:52 -05:00
9bd554b513 Add injectivity lemma for abs
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 21:31:36 -05:00
300530a93f Finish off some easy contradictory cases
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 21:11:36 -05:00
f0c18fd77e Finish the neutral app case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 20:42:08 -05:00
8d765c495d Add some more injection lemmas for neutrals
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 19:08:49 -05:00
186f2138e6 Finish the var base case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 16:58:07 -05:00
8fd6919538 Make progress on coqeq_complete
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 16:17:21 -05:00
ea14ba9602 Prove most of cases of AbsAbs
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 14:49:36 -05:00
5ed366f093 Prove some easy cases of completeness