Skip to content

proof(L2): TypingL2.v + Modality.v skeleton — Linear⇒Affine weakening Qed#168

Merged
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l2-modality-skeleton
May 27, 2026
Merged

proof(L2): TypingL2.v + Modality.v skeleton — Linear⇒Affine weakening Qed#168
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l2-modality-skeleton

Commits

Commits on May 27, 2026