The following code is non-functional, just a sketch:

```
class Subgroup : Definition
{
public:
Set G;
Set H;
private:
Assert[] given = [G in Grp("G"), H=subset(G, "H")];
Assert[] input = [[a,b] in H >>> a*(b^(-1)) in H]];
Assert[] output = [H ~ " is a subgroup of " ~ G];
Notate[] denoted = [H ~ r"\leqslant " ~ G];
}
```

There will be a gigantic brain-like graph. Nodes with I/O. For each new Definition/Assertion made by the user, I would like them to be automatically wired-into the brain graph up to variable substitution. So it's not as simple as using an AA to accomplish this. And I don't want to loop through all nodes and then check for all outputs that match the inputs, etc. So can you think of a way to accomplish this, especially that is D-friendly?

Up to variable substitution means there is a mechanism that knows that "A is a subgroup of B" is essentially the same thing as "H is a subgroup of G", you simply map the variables appropriately.