Declthird_probeAxiomsfree
(n m : Nat) →
@Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n m)
(@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) m n)Thesis
- Declthird_probeDeclaration kindtheorem
(n m : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n m) (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) m n)
DOIMTH.R-2026-6502
Cite
Verification
- Replay
- accepted
- Axioms
- free
- Statement identity
- not-applicable
- Statement source
- kernel
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- deposit@v4.31.0 · deposit
- Frozen export
- 731ef5186ce1
- Verified
- 2026-09-29T21:58:45Z
- Deposited source
- https://mathesis.noumenal.world/deposits/5