proof(L1.F): discharge loc_retype_at_R_l1 axiom via region-liveness invariant#162

hyperpolymath merged 1 commit into

proof/l1-region-threading-designhyperpolymath/ephapax:proof/l1-region-threading-designfrom

proof/l1f-region-livenesshyperpolymath/ephapax:proof/l1f-region-livenessCopy head branch name to clipboard