{-# OPTIONS --safe #-}

open import Prelude
open import Data.Vec
open import Signatures

module FreeMonad.FindVars {𝔽 : Signature} where

open import FreeMonad.Syntax 𝔽
open import FreeMonad.Theory

FindVars : Theory 𝔽 a → _
FindVars 𝒯 = ∀ i (γ : Γ (𝒯 .Theory.Eqns i)) → Discrete (ν (𝒯 .Theory.Eqns i) γ)