/-
Copyright (c) 2026 SilverSight. All rights reserved.
Released under Apache 2.0 license.

Discharge gate: each frozen theorem is matched to its proof by `rfl`.
If the types don't match exactly, this file fails to compile.
-/
import ModuleName.Theorems
import ModuleName.Proofs.Basic

open ModuleName

/-! ## Discharge gates -/

theorem my_theorem : my_theorem = my_theorem_proof := rfl
lemma my_lemma : my_lemma = my_lemma_proof := rfl