pub trait ProofRule<Split: SplitStrategy>: CheckerRule {
// Required methods
fn applicable(&self, term: &Term) -> bool;
fn prove<'t>(
&self,
checker: CheckRef<'t, '_, Split>,
goal: &'t Term,
) -> Option<Term>;
}