proofs(lean4): close ET-2 — L1 conversion is decidable#24

hyperpolymath merged 1 commit into

proofs/lean4-l1-l2hyperpolymath/systemet:proofs/lean4-l1-l2from

proofs/et2-conversion-et14-teahyperpolymath/systemet:proofs/et2-conversion-et14-teaCopy head branch name to clipboard